
\chapter{The logic of types. III. The Curry-Howard correspondence\label{chap:5-Curry-Howard}}

\global\long\def\gunderline#1{\mathunderline{greenunder}{#1}}%
\global\long\def\bef{\forwardcompose}%
\global\long\def\bbnum#1{\custombb{#1}}%
Fully parametric functions (introduced in Section~\ref{sec:Fully-parametric-functions})
perform operations so general that their code does not depend on values
of any specific data types such as \lstinline!Int! or \lstinline!String!.
An example of a fully parametric function is
\begin{lstlisting}
def before[A, B, C](f: A => B, g: B => C): A => C = { x => g(f(x)) }
\end{lstlisting}
We have also seen in Section~\ref{subsec:Deriving-a-function-s-code}
that for certain functions of this kind, the code can be derived unambiguously
from the type signature.

There exists a mathematical theory (called the \textbf{Curry-Howard
correspondence}) that gives precise conditions for the possibility
of deriving a function\textsf{'}s code from its type, and a systematic derivation
algorithm. Technical details about the algorithm are in Appendix~\ref{app:CH-correspondence-LJT-algorithm}.
This chapter describes the main results and applications of that theory
to functional programming.

\section{Values computed by fully parametric functions}

\subsection{Motivation}

Consider possible Scala code for a fully parametric function,

\begin{wrapfigure}{l}{0.54\columnwidth}%
\vspace{-0.65\baselineskip}
\begin{lstlisting}
def f[A, B, ...]: ... = {
  val x: Either[A, B] = ... // Some expression here.
  ... }
\end{lstlisting}

\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent If this program compiles without type errors, it means that
the types match and, in particular, that the function \lstinline!f!
is able to compute a value \lstinline!x! of type \lstinline!Either[A, B]!.

It is sometimes \emph{impossible} to compute a value of a certain
type within the body of a fully parametric function. For example,
the fully parametric function \lstinline!fmap! shown in Section~\ref{subsec:Disjunctive-Example-option-1}
cannot compute any values of type \lstinline!A!,

\begin{wrapfigure}{l}{0.54\columnwidth}%
\vspace{-0.65\baselineskip}
\begin{lstlisting}
def fmap[A, B](f: A => B): Option[A] => Option[B] = {
  val x: A = ??? // Cannot compute x here!
  ... }
\end{lstlisting}

\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent The reason is that a fully parametric function cannot compute
values of type \lstinline!A! from scratch without using previously
given values of type \lstinline!A! and without applying a function
that returns values of type \lstinline!A!. In \lstinline!fmap!,
no values of type \lstinline!A! are given as arguments; the given
function \lstinline!f: A => B! returns values of type \lstinline!B!
and not \lstinline!A!. The code of \lstinline!fmap! must perform
pattern matching on a value of type \lstinline!Option[A]!:

\begin{wrapfigure}{l}{0.54\columnwidth}%
\vspace{-0.65\baselineskip}
\begin{lstlisting}
def fmap[A, B](f: A => B): Option[A] => Option[B] = {
  case None       => 
    val x: A = ??? // Cannot compute x here!
    ...
  case Some(a)    =>
    val x: A = a   // Can compute x in this scope.
    ... }
\end{lstlisting}

\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent Since the case \lstinline!None! has no values of type \lstinline!A!,
we are unable to compute a value \lstinline!x! in that scope (as
long as \lstinline!fmap! remains a fully parametric function). 

Being able to compute \lstinline!x:A! \textsf{``}within the body of a function\textsf{''}
means that, if needed, the function should be able to \emph{return}
\lstinline!x! as a result value. This requires computing \lstinline!x!
in all cases, not just within one part of the \lstinline!match! expression. 

The body of \lstinline!fmap! also cannot compute any values of type
\lstinline!B!. Since no arguments of type \lstinline!B! are given,
the only way of obtaining a value of type \lstinline!B! would be
to apply the function \lstinline!f: A => B! to \emph{some} value
of type \lstinline!A!; but we just saw that the body of \lstinline!fmap!
cannot compute any values of type \lstinline!A!.

Another example where one cannot compute a value of a certain type
is in the following code:

\begin{wrapfigure}{l}{0.54\columnwidth}%
\vspace{-0.1\baselineskip}
\begin{lstlisting}
def before[A, B, C](f: A => B, g: B => C): A => C = {
  //  val h: C => A = ???   // Cannot compute h here!
  a => g(f(a)) // Can compute a value of type A => C.
}
\end{lstlisting}

\vspace{-1.2\baselineskip}
\end{wrapfigure}%

\noindent The body of \lstinline!before! may only use the arguments
\lstinline!f! and \lstinline!g!. We can compose \lstinline!f! and
\lstinline!g! to get a value of type \lstinline!A => C!; but it
is impossible to compute a value \lstinline!h! of type \lstinline!C => A!,
no matter what code we try to write. The reason is that the body of
\lstinline!before! has no given values of type \lstinline!A! and
no functions that return values of type \lstinline!A!, so a nameless
function such as \lstinline!{c:C => ???}! cannot compute its return
value of type \lstinline!A!. Since a fully parametric function cannot
create values of an arbitrary type \lstinline!A! from scratch, we
see no possibility of computing \lstinline!h! within the body of
\lstinline!before!.

Can we prove rigorously that a value of type \lstinline!C => A! cannot
be computed within the body of \lstinline!before!? Or, perhaps, a
clever trick \emph{could} produce a value of that type? So far, we
only saw informal arguments about whether values of certain types
can be computed. To make the arguments rigorous, we need to translate
statements such as \textsf{``}\emph{a fully parametric function} \lstinline!before!
\emph{can compute a value of type} \lstinline!C => A!\textsf{''} into mathematical
formulas, with rigorous rules for proving them true or false.

In Section~\ref{subsec:Disjunctions-and-conjunctions}, we denoted
by ${\cal CH}(A)$ the proposition \textsf{``}the ${\cal C}$ode ${\cal H}$as
a value of type $A$\textsf{''}. By \textsf{``}the code\textsf{''} we now mean the body of
a given fully parametric function. So, the notation ${\cal CH}(A)$
is not completely adequate because the validity of the proposition
${\cal CH}(A)$ depends not only on the choice of the type $A$ but
also on the place in the code fragment where the value of type $A$
needs to be computed. What exactly is this additional dependency?
In the above examples, we used the \emph{types} of a function\textsf{'}s arguments
when reasoning about getting a value of a given type $A$. Thus, a
precise description of the proposition ${\cal CH}(A)$ is 
\begin{align}
{\color{greenunder}{\cal CH}\text{-proposition}:}\quad & \text{a fully parametric function having arguments of types}\nonumber \\
 & X,Y,...,Z\text{ can compute a value of type }A\quad.\label{eq:ch-CH-proposition-def}
\end{align}
Here $X$, $Y$, ..., $Z$, $A$ may be either type parameters or
more complicated type expressions such as $B\rightarrow C$ or $(C\rightarrow D)\rightarrow E$,
built from other type parameters.

If arguments of types $X$, $Y$, ..., $Z$ are given, it means we
already have values of those types. So, the propositions ${\cal CH}(X)$,
${\cal CH}(Y)$, ..., ${\cal CH}(Z)$ will be true. Thus, proposition~(\ref{eq:ch-CH-proposition-def})
is equivalent to \textsf{``}${\cal CH}(A)$ is true, assuming ${\cal CH}(X)$,
${\cal CH}(Y)$, ..., ${\cal CH}(Z)$ are true\textsf{''}. In mathematical
logic, a statement of this form is called a \textbf{sequent} and is
denoted using the symbol $\vdash$ (the \textsf{``}turnstile\textsf{''}):
\begin{equation}
{\cal CH}(X),{\cal CH}(Y),...,{\cal CH}(Z)\vdash{\cal CH}(A)\quad.\label{eq:ch-example-sequent}
\end{equation}
The assumptions ${\cal CH}(X)$, ${\cal CH}(Y)$, ..., ${\cal CH}(Z)$
are called \textbf{premises}\index{sequent (in logic)!premises} and
the proposition ${\cal CH}(A)$ is called the \textbf{goal}\index{sequent (in logic)!goal}
of the sequent. Showing rigorously the possibility of computing values
in functions means proving sequents of the form~(\ref{eq:ch-example-sequent}).
Our previous examples are denoted by the following sequents:
\begin{align*}
{\color{greenunder}\text{\texttt{fmap} for \texttt{Option}}:}\quad & {\cal CH}(\text{\texttt{A => B}})\vdash{\cal CH}(\text{\texttt{Option[A] => Option[B]}})\\
{\color{greenunder}\text{the function \texttt{before}}:}\quad & {\cal CH}(\text{\texttt{A => B}}),{\cal CH}(\text{\texttt{B => C}})\vdash{\cal CH}(\text{\texttt{A => C}})\\
{\color{greenunder}\text{value of type }A\text{ within \texttt{fmap}}:}\quad & {\cal CH}(\text{\texttt{A => B}}),{\cal CH}(\text{\texttt{Option[A]}})\vdash{\cal CH}(\text{\texttt{A}})\\
{\color{greenunder}\text{value of type }C\rightarrow A\text{ within \texttt{before}}:}\quad & {\cal CH}(\text{\texttt{A => B}}),{\cal CH}(\text{\texttt{B => C}})\vdash{\cal CH}(\text{\texttt{C => A}})
\end{align*}
Calculations in formal logic are called \textbf{proofs}\index{proof (in logic)}.
So, in this section we gave informal arguments towards proving the
first two sequents and disproving the last two. We will now develop
tools for rigorous reasoning about sequents.

A proposition ${\cal CH}(A)$ may be true with one set of premises
such as ${\cal CH}(X)$, ${\cal CH}(Y)$, ..., ${\cal CH}(Z)$ but
false with another. Here and in the following sections, we will be
reasoning about ${\cal CH}$-propositions within the body of a \emph{chosen}
fully parametric function, i.e., with a fixed set of premises. We
will then temporarily omit the premises and use the shorter notation
${\cal CH}(A)$.

\subsection{Type notation and ${\cal CH}$-propositions for standard type constructions\label{subsec:Type-notation-and-standard-type-constructions}}

In Section~\ref{subsec:Disjunctions-and-conjunctions} we saw examples
of reasoning about ${\cal CH}$-propositions for case classes and
for disjunctive types. We will now extend this reasoning systematically
to all type constructions that programs could use. A special type
notation\index{type notation} explained in this section will help
us write type expressions more concisely. (See Appendix~\ref{chap:Appendix-Notations}
for reference on the type notation.)

There are six \textbf{standard type constructions}\index{six type constructions}
supported by all functional languages: primitive types (including
\lstinline!Unit! type and the void type, called \lstinline!Nothing!
in Scala), product (tuple) types, co-product (disjunctive) types,
function types, parameterized types, and recursive types. We will
now derive the rules for writing ${\cal CH}$-propositions for each
of these type constructions (except recursive types).

\paragraph{1a) Rule for the \texttt{Unit} type}

The \lstinline!Unit! type has only a single value \lstinline!()!,
an \textsf{``}empty tuple\textsf{''}. This value can be \emph{always} computed since
it does not need any previous data:
\begin{lstlisting}
def f[...]: ... = {
  ...
  val x: Unit = () // We can always compute a `Unit` value.
  ...
\end{lstlisting}
So, the proposition ${\cal CH}($\lstinline!Unit!$)$ is always true.
In the type notation, the \lstinline!Unit! type is denoted by $\bbnum 1$.
We may write $\mathcal{CH}(\bbnum 1)=True$.

Named unit types\index{unit type!named} also have a single value
that is always possible to compute. For example,
\begin{lstlisting}
final case class N1()
\end{lstlisting}
defines a named unit type; we can compute

\begin{wrapfigure}{l}{0.42\columnwidth}%
\vspace{-0.7\baselineskip}
\begin{lstlisting}
val x: N1 = N1()
\end{lstlisting}

\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent So, the proposition ${\cal CH}($\lstinline!N1!$)$ is
always true. Named unit types are also denoted by $\bbnum 1$, just
as the \lstinline!Unit! type itself.

\paragraph{1b) Rule for the void type}

The Scala type \lstinline!Nothing! has no values, so the proposition
${\cal CH}($\lstinline!Nothing!$)$ is always false. The type \lstinline!Nothing!
is denoted by $\bbnum 0$ in the type notation. So, the rule is $\mathcal{CH}(\bbnum 0)=False$.

\paragraph{1c) Rule for primitive types}

For a specific primitive (or library-defined) type such as \lstinline!Int!
or \lstinline!String!, the corresponding ${\cal CH}$-proposition
is \emph{always true} because we could use a constant value, e.g.:
\begin{lstlisting}
def f[...]: ... {
   ...
   val x: String = "abc" // We can always compute a `String` value.
   ...
\end{lstlisting}
So, the rule for primitive types is the same as that for the \lstinline!Unit!
type. For example, $\mathcal{CH}(\text{String})=True$.

\paragraph{2) Rule for tuple types}

To compute a value of a tuple type \lstinline!(A, B)! requires computing
a value of type \lstinline!A! \emph{and} a value of type \lstinline!B!.
This is expressed by the logic formula ${\cal CH}($\lstinline!(A, B)!$)={\cal CH}(A)\wedge{\cal CH}(B)$.
A similar formula holds for case classes, as Eq.~(\ref{eq:curry-howard-example-case-class})
shows. In the type notation, the tuple \lstinline!(A, B)! is written
as $A\times B$. Tuples and case classes with more than two parts
are denoted similarly as $A\times B\times...\times C$. For example,
the Scala definition
\begin{lstlisting}
case class Person(firstName: String, lastName: String, age: Int)
\end{lstlisting}
is written in the type notation as $\text{String}\times\text{String}\times\text{Int}$.
So, the rule for tuple types is
\[
{\cal CH}\left(A\times B\times...\times C\right)={\cal CH}(A)\wedge{\cal CH}(B)\wedge...\wedge{\cal CH}(C)\quad.
\]


\paragraph{3) Rule for disjunctive types}

A disjunctive type may consist of several case classes. Having a value
of a disjunctive type means to have a value of (at least) one of those
case classes. An example of translating this relationship into a formula
was shown by Eq.~(\ref{eq:curry-howard-example-disjunction}). For
the standard disjunctive type \lstinline!Either[A, B]!, we have the
logical formula ${\cal CH}($\lstinline!Either[A, B]!$)={\cal CH}(A)\vee{\cal CH}(B)$.
In the type notation, the Scala type \lstinline!Either[A, B]! is
written as $A+B$. A longer example: the Scala definition
\begin{lstlisting}
sealed trait RootsOfQ
final case class NoRoots()                      extends RootsOfQ
final case class OneRoot(x: Double)             extends RootsOfQ
final case class TwoRoots(x: Double, y: Double) extends RootsOfQ
\end{lstlisting}
is translated to the type notation as
\[
\text{RootsOfQ}=1+\text{Double}+\text{Double}\times\text{Double}\quad.
\]
Here, the type notation is significantly shorter because it omits
all case class names and part names from the type definitions. In
this notation, the rule for disjunctive types is
\[
{\cal CH}\left(A+B+...+C\right)={\cal CH}(A)\vee{\cal CH}(B)\vee...\vee{\cal CH}(C)\quad.
\]


\paragraph{4) Rule for function types}

Consider now a function type such as \lstinline!A => B!. (This type
is written in the type notation as $A\rightarrow B$.) To compute
a value of that type, we need to write code like this:

\begin{wrapfigure}{l}{0.5\columnwidth}%
\vspace{-0.65\baselineskip}
\begin{lstlisting}
val f: A => B = { (a: A) =>
  ??? // Compute a value of type B in this scope.
}
\end{lstlisting}

\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent The inner scope of the function needs to compute a value
of type $B$, and the given value \lstinline!a:A! may be used for
that. So, ${\cal CH}(A\rightarrow B)$ is true if and only if we are
able to compute a value of type $B$ when we are given a value of
type $A$. To translate this statement into the language of logical
propositions, we need to use the logical\index{logical implication}
\textbf{implication}, ${\cal CH}(A)\Rightarrow{\cal CH}(B)$, which
means that ${\cal CH}(B)$ can be proved if ${\cal CH}(A)$ already
holds. So the rule for function types is
\[
{\cal CH}(A\rightarrow B)={\cal CH}(A)\Rightarrow{\cal CH}(B)\quad.
\]


\paragraph{5) Rule for parameterized types}

Consider a function with type parameters, for instance:
\begin{lstlisting}
def f[A, B]: A => (A => B) => B = { x => g => g(x) }
\end{lstlisting}
Being able to define the body of such a function is the same as being
able to compute a value of type \lstinline!A => (A => B) => B! for
\emph{all} possible types \lstinline!A! and \lstinline!B!. In the
notation of formal logic, this is written as
\[
{\cal CH}\left(\forall(A,B).\,A\rightarrow(A\rightarrow B)\rightarrow B\right)
\]
and is equivalent to
\[
\forall(A,B).\,{\cal CH}\left(A\rightarrow(A\rightarrow B)\rightarrow B\right)\quad.
\]
The symbol $\forall$ means \textsf{``}for all\textsf{''} and is known as the \index{universal quantifier}\textbf{universal
quantifier} in logic. 

The code notation for the parameterized function \lstinline!f! is
\[
f^{A,B}:A\rightarrow\left(A\rightarrow B\right)\rightarrow B\quad,
\]
and its type signature can be written as
\[
\forall(A,B).\,A\rightarrow\left(A\rightarrow B\right)\rightarrow B\quad.
\]

In Scala, longer type expressions can be named and their names (called
\textbf{type aliases}\index{type alias}) can be used to make code
shorter. Type aliases may also contain type parameters. Defining and
using a type alias for the type of the function \lstinline!f! looks
like this:
\begin{lstlisting}
type F[A, B] = A => (A => B) => B
def f[A, B]: F[A, B] = { x => g => g(x) }
\end{lstlisting}
This is written in the type notation by placing all type parameters
into superscripts:
\begin{align*}
F^{A,B} & \triangleq A\rightarrow\left(A\rightarrow B\right)\rightarrow B\quad,\\
f^{A,B}:F^{A,B} & \triangleq x^{:A}\rightarrow g^{:A\rightarrow B}\rightarrow g(x)\quad,
\end{align*}
or equivalently (although somewhat less readably) as
\[
f:\big(\forall(A,B).\,F^{A,B}\big)\triangleq\forall(A,B).\,x^{:A}\rightarrow g^{:A\rightarrow B}\rightarrow g(x)\quad.
\]

In Scala 3, the function \lstinline!f! can be written as a value
(\lstinline!val!) via this syntax:
\begin{lstlisting}
val f: [A, B] => A => (A => B) => B = {   // Valid only in Scala 3.
  [A, B] => (x: A) => (g: A => B) => g(x)
}
\end{lstlisting}
This syntax corresponds more closely to the code notation $\forall(A,B).\,x^{:A}\rightarrow g^{:A\rightarrow B}\rightarrow g(x)$.

So, the rule for parameterized types with the type notation $F^{A}$
is
\[
{\cal CH}(\forall A.\,F^{A})=\forall A.\,{\cal CH}(F^{A})\quad.
\]

Case classes and disjunctive types use \emph{names} for the types
and their parts. However, those names only add convenience for programmers
and do not affect the computational properties of types. The type
notation is designed to support nameless type expressions.

Table~\ref{tab:ch-correspondence-type-notation-CH-propositions}
summarizes the type notation and also shows how to translate it into
logic formulas with propositions of the form ${\cal CH}(...)$.

The precedence\index{type notation!operator precedence} of operators
in the type notation is chosen to have fewer parentheses in the type
expressions that are frequently used. The rules of precedence are:
\begin{itemize}
\item The type product operator ($\times$) groups stronger than the disjunctive
operator ($+$), so that type expressions such as $A+B\times C$ have
the same operator precedence as in standard arithmetic. That is, $A+B\times C$
means $A+\left(B\times C\right)$. This convention makes type expressions
easier to reason about (for people familiar with arithmetic).
\item The function type arrow ($\rightarrow$) groups weaker than the operators
$+$ and $\times$, so that often-used types such as $A\rightarrow\bbnum 1+B$
(representing \lstinline!A => Option[B]!) or $A\times B\rightarrow C$
(representing \lstinline!((A, B)) => C!) can be written without any
parentheses. Type expressions such as $\left(A\rightarrow B\right)\times C$
will require parentheses but are needed less often.
\item The type quantifiers group weaker than all other operators, so we
can write types such as $\forall A.\,A\rightarrow A\rightarrow A$
without parentheses. Type quantifiers are most often placed outside
a type expression. When this is not the case, parentheses are necessary,
e.g., in the type expression $\left(\forall A.\,A\rightarrow A\rightarrow A\right)\rightarrow\bbnum 1+\bbnum 1$.
\end{itemize}
\begin{table}
\begin{centering}
\begin{tabular}{|c|c|c|c|}
\hline 
\textbf{\small{}Type construction} & \textbf{\small{}Scala syntax} & \textbf{\small{}Type notation} & \textbf{\small{}${\cal CH}$-proposition}\tabularnewline
\hline 
\hline 
{\small{}type parameter} & \lstinline![A]! & $A$ & ${\cal CH}(A)$\tabularnewline
\hline 
{\small{}product type (tuple)}  & \lstinline!(A, B)! & $A\times B$ & ${\cal CH}(A)$ $\wedge$ ${\cal CH}(B)$\tabularnewline
\hline 
{\small{}disjunctive type}  & \lstinline!Either[A, B]! & $A+B$ & ${\cal CH}(A)$ $\vee$ ${\cal CH}(B)$\tabularnewline
\hline 
{\small{}function type}  & \lstinline!A => B! & $A\rightarrow B$ & ${\cal CH}(A)$ $\Rightarrow$ ${\cal CH}(B)$\tabularnewline
\hline 
{\small{}unit or a \textsf{``}named unit\textsf{''} type} & \lstinline!Unit! & $\bbnum 1$ & ${\cal CH}(\bbnum 1)=True$\tabularnewline
\hline 
{\small{}primitive type} & {\small{}}\lstinline!Int!{\small{}, }\lstinline!String!{\small{},
...} & {\small{}$\text{Int}$, $\text{String}$, ...} & ${\cal CH}(\text{Int})=True$\tabularnewline
\hline 
{\small{}void type} & \lstinline!Nothing! & $\bbnum 0$ & ${\cal CH}(\bbnum 0)=False$\tabularnewline
\hline 
{\small{}value parameterized by type} & \lstinline!def f[A]: F[A]! & $f^{A}:F^{A}$ & $\forall A.\,{\cal CH}(F^{A})$\tabularnewline
\hline 
{\small{}type with quantifier} & \lstinline![A] => F[A]!{\small{} (Scala 3)} & $\forall A.\,F^{A}$ & $\forall A.\,{\cal CH}(F^{A})$\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{The correspondence\index{type notation} between type constructions
and ${\cal CH}$-propositions.\label{tab:ch-correspondence-type-notation-CH-propositions}}
\end{table}


\subsection{Solved examples: Type notation\index{solved examples}}

From now on, we will prefer to write types in the type notation rather
than in the Scala syntax. The type notation allows us to write nameless
type expressions and, in particular, makes the structure of disjunctive
types and their parts more clear, compared with the Scala syntax.
Names of types and parts of types are, of course, helpful for reminding
the programmer of the meaning of data in a program. However, writing
names for every part of every type is not helpful for reasoning about
the properties of types. Type notation makes reasoning about types
easier, as we will see throughout this chapter. Once the programmer
has finished deriving the necessary types and verifying their properties,
the type expressions can be straightforwardly translated from the
type notation into Scala code.

Let us get some experience converting between type notation and Scala
code.

\subsubsection{Example \label{subsec:Example-ch-dupl-function}\ref{subsec:Example-ch-dupl-function}}

Define a function \lstinline!delta! taking an argument \lstinline!x!
and returning the pair \lstinline!(x, x)!. Derive the most general
type for this function. Write the type signature of \lstinline!delta!
in the type notation, and translate it into a ${\cal CH}$-proposition.
Simplify the ${\cal CH}$-proposition if possible.

\subparagraph{Solution}

Begin by writing the code of the function:
\begin{lstlisting}
def delta(x: ...) = (x, x)
\end{lstlisting}
To derive the most general type for \lstinline!delta!, first assume
\lstinline!x:A!, where \lstinline!A! is a type parameter; then the
tuple \lstinline!(x, x)! has type \lstinline!(A, A)!. We do not
see any constraints on the type parameter \lstinline!A!. So the type
parameter represents an arbitrary type and needs to be added to the
type signature of \lstinline!delta!:
\begin{lstlisting}
def delta[A](x: A): (A, A) = (x, x)
\end{lstlisting}
We find that the most general type of \lstinline!delta! is \lstinline!A => (A, A)!.
We also note that there is only one way of implementing a fully parametric
function with type signature \lstinline!A => (A, A)!: the function
must duplicate its given argument.

It is convenient to use the letter $\Delta$ for the function \lstinline!delta!.
In the type notation, the type signature of $\Delta$ is written as
\[
\Delta^{A}:A\rightarrow A\times A\quad.
\]
So the proposition ${\cal CH}(\Delta)$ (meaning \textsf{``}the function $\Delta$
can be implemented\textsf{''}) is
\[
{\cal CH}(\Delta)=\forall A.{\cal \,CH}\left(A\rightarrow A\times A\right)\quad.
\]
In the type expression $A\rightarrow A\times A$, the product symbol
($\times$) binds stronger than the function arrow ($\rightarrow$),
so the parentheses in $A\rightarrow\left(A\times A\right)$ may be
omitted.

Using the rules for transforming ${\cal CH}$-propositions, we rewrite
\begin{align*}
 & {\cal CH}(A\rightarrow A\times A)\\
{\color{greenunder}\text{rule for function types}:}\quad & ={\cal CH}(A)\Rightarrow{\cal CH}(A\times A)\\
{\color{greenunder}\text{rule for tuple types}:}\quad & ={\cal CH}(A)\Rightarrow\left({\cal CH}(A)\wedge{\cal CH}(A)\right)\quad.
\end{align*}
Thus the proposition ${\cal CH}(\Delta)$ is equivalent to
\[
{\cal CH}(\Delta)=\forall A.\,{\cal CH}(A)\Rightarrow({\cal CH}(A)\wedge{\cal CH}(A))\quad.
\]


\subsubsection{Example \label{subsec:Example-ch-notation-function-1}\ref{subsec:Example-ch-notation-function-1}}

The standard disjunctive types \lstinline!Either[A, B]! and \lstinline!Option[A]!
are written in the type notation as
\[
\text{Either}^{A,B}\triangleq A+B\quad,\quad\quad\text{Opt}^{A}\triangleq\bbnum 1+A\quad.
\]
The type \lstinline!Either[A, B]! is written as $A+B$ by definition
of the disjunctive type notation ($+$). The type \lstinline!Option[A]!
has two disjoint cases, \lstinline!None! and \lstinline!Some[A]!.
The case class \lstinline!None! is a \textsf{``}\index{unit type!named}named
\lstinline!Unit!\textsf{''} and is denoted by $\bbnum 1$. The case class
\lstinline!Some[A]! contains a single value of type $A$. So, the
type notation for \lstinline!Option[A]! is $\bbnum 1+A$. We will
also sometimes write $\text{Opt}^{A}$ to denote \lstinline!Option[A]!.

\subsubsection{Example \label{subsec:Example-ch-notation-function-1-a}\ref{subsec:Example-ch-notation-function-1-a}}

The Scala definition of the disjunctive type \lstinline!UserAction!,
\begin{lstlisting}
sealed trait UserAction
final case class SetName(first: String, last: String) extends UserAction
final case class SetEmail(email: String)              extends UserAction
final case class SetUserId(id: Long)                  extends UserAction
\end{lstlisting}
is written in the type notation as
\begin{equation}
\text{UserAction}\triangleq\text{String}\times\text{String}+\text{String}+\text{Long}\quad.\label{eq:ch-example-case-class-type-notation}
\end{equation}
The type operation $\times$ groups stronger than $+$, as in arithmetic.
To derive the type notation~(\ref{eq:ch-example-case-class-type-notation}),
we first drop all names from case classes and get three nameless tuples
\lstinline!(String, String)!, \lstinline!(String)!, and \lstinline!(Long)!.
Each of these tuples is then converted into a product using the operator
$\times$, and all products are \textsf{``}summed\textsf{''} in the type notation
using the operator $+$.

\subsubsection{Example \label{subsec:Example-ch-notation-function-2}\ref{subsec:Example-ch-notation-function-2}}

The parameterized disjunctive type \lstinline!Either3! is a generalization
of \lstinline!Either!:
\begin{lstlisting}
sealed trait Either3[A, B, C]
final case class Left[A, B, C](x: A)   extends Either3[A, B, C]
final case class Middle[A, B, C](x: B) extends Either3[A, B, C]
final case class Right[A, B, C](x: C)  extends Either3[A, B, C]
\end{lstlisting}
This disjunctive type is written in the type notation as
\[
\text{Either3}^{A,B,C}\triangleq A+B+C\quad.
\]


\subsubsection{Example \label{subsec:Example-ch-notation-function-3}\ref{subsec:Example-ch-notation-function-3}}

Define a Scala type constructor \lstinline!F[A]! corresponding to
the type notation 
\[
F^{A}\triangleq\bbnum 1+\text{Int}\times A\times A+\text{Int}\times\left(\text{Int}\rightarrow A\right)\quad.
\]


\subparagraph{Solution}

The formula for $F^{A}$ defines a disjunctive type \lstinline!F[A]!
with three parts. To implement \lstinline!F[A]! in Scala, we need
to choose names for each of the disjoint parts, which will become
case classes. For the purposes of this example, let us choose names
\lstinline!F1!, \lstinline!F2!, and \lstinline!F3!. Each of these
case classes needs to have the same type parameter \lstinline!A!.
So we begin writing the code as
\begin{lstlisting}
sealed trait F[A]
final case class F1[A](...) extends F[A]
final case class F2[A](...) extends F[A]
final case class F3[A](...) extends F[A]
\end{lstlisting}
Each of these case classes represents one part of the disjunctive
type: \lstinline!F1! represents $\bbnum 1$, \lstinline!F2! represents
$\text{Int}\times A\times A$, and \lstinline!F3! represents $\text{Int}\times\left(\text{Int}\rightarrow A\right)$.
To define these case classes, we need to name their parts. The final
code is
\begin{lstlisting}
sealed trait F[A]
final case class F1[A]()                     extends F[A]  // Named unit type.
final case class F2[A](n: Int, x1: A, x2: A) extends F[A]
final case class F3[A](n: Int, f: Int => A)  extends F[A]
\end{lstlisting}
The names \lstinline!n!, \lstinline!x1!, \lstinline!x2!, and \lstinline!f!
are chosen purely for convenience.

\subsubsection{Example \label{subsec:Example-ch-notation-function-4}\ref{subsec:Example-ch-notation-function-4}}

Write the type signature of the function
\begin{lstlisting}
def fmap[A, B](f: A => B): Option[A] => Option[B]
\end{lstlisting}
in the type notation.

\subparagraph{Solution}

This is a curried function, so we first rewrite the type signature
as
\begin{lstlisting}
def fmap[A, B]: (A => B) => Option[A] => Option[B]
\end{lstlisting}
The type notation for \lstinline!Option[A]! is $\bbnum 1+A$. Now
we can write the type signature of \lstinline!fmap! as
\begin{align*}
 & \text{fmap}^{A,B}:\left(A\rightarrow B\right)\rightarrow\bbnum 1+A\rightarrow\bbnum 1+B\quad,\\
{\color{greenunder}\text{or equivalently}:}\quad & \text{fmap}:\forall(A,B).\,\left(A\rightarrow B\right)\rightarrow\bbnum 1+A\rightarrow\bbnum 1+B\quad.
\end{align*}
We do not put parentheses around $\bbnum 1+A$ and $\bbnum 1+B$ because
the function arrow ($\rightarrow$) groups weaker than the other type
operations. Parentheses around $\left(A\rightarrow B\right)$ are
required.

We will usually prefer to write type parameters in superscripts rather
than under type quantifiers. So, for example, we will write $\text{id}^{A}\triangleq x^{:A}\rightarrow x$
rather than $\text{id}\triangleq\forall A.\,x^{:A}\rightarrow x$.

\subsection{Exercises: Type notation\index{exercises}}

\subsubsection{Exercise \label{subsec:Exercise-type-notation-1}\ref{subsec:Exercise-type-notation-1}}

Define a Scala disjunctive type \lstinline!Q[T, A]! corresponding
to the type notation
\[
Q^{T,A}\triangleq\bbnum 1+T\times A+\text{Int}\times(T\rightarrow T)+\text{String}\times A\quad.
\]


\subsubsection{Exercise \label{subsec:Exercise-type-notation-2}\ref{subsec:Exercise-type-notation-2}}

Rewrite \lstinline!Either[(A, Int), Either[(A, Char), (A, Float)]]!
in the type notation. 

\subsubsection{Exercise \label{subsec:Exercise-type-notation-3}\ref{subsec:Exercise-type-notation-3}}

Define a Scala type \lstinline!Opt2[A, B]! written in the type notation
as $\bbnum 1+A+B$.

\subsubsection{Exercise \label{subsec:Exercise-type-notation-4}\ref{subsec:Exercise-type-notation-4}}

Write a Scala type signature for the fully parametric function 
\[
\text{flatMap}^{A,B}:\bbnum 1+A\rightarrow\left(A\rightarrow\bbnum 1+B\right)\rightarrow\bbnum 1+B
\]
and implement this function, preserving information as much as possible.

\section{The logic of ${\cal CH}$-propositions}

\subsection{Motivation and first examples\label{subsec:ch-Motivation-and-first-examples}}

So far, we were able to convert statements such as \textsf{``}\emph{a fully
parametric function can compute values of type} $A$\textsf{''} into logical
propositions of the form ${\cal CH}(A)$ that we called ${\cal CH}$-propositions.
The next step is to determine the proof rules suitable for reasoning
about ${\cal CH}$-propositions.

Formal logic uses axioms and derivation rules for proving that certain
formulas are true or false. A simple example of a true formula is
\textsf{``}any proposition $\alpha$ is equivalent to itself\textsf{''},
\[
\forall\alpha.\,\alpha=\alpha\quad.
\]
In logic, equivalence of propositions is usually understood\index{implication (in logic)}
as \index{logical implication}\textbf{implication} ($\Rightarrow$)
in both directions: $\alpha=\beta$ means $\left(\alpha\Rightarrow\beta\right)\wedge\left(\beta\Rightarrow\alpha\right)$.
So, the above formula is the same as
\[
\forall\alpha.\,\alpha\Rightarrow\alpha\quad.
\]
If the proposition $\alpha$ is a ${\cal CH}$-proposition, $\alpha\triangleq{\cal CH}(A)$
for some type $A$, we obtain the formula
\begin{equation}
\forall A.\,{\cal CH}(A)\Rightarrow{\cal CH}(A)\quad.\label{eq:ch-type-sig-1}
\end{equation}
We expect true ${\cal CH}$-propositions to correspond to types that
\emph{can} be computed in a fully parametric function. Let us see
if this example fits our expectations. We can rewrite Eq.~(\ref{eq:ch-type-sig-1})
as
\begin{align*}
 & \forall A.\,\gunderline{{\cal CH}(A)\Rightarrow{\cal CH}(A)}\\
{\color{greenunder}\text{rule for function types}:}\quad & =\gunderline{\forall A}.\,{\cal CH}\left(A\rightarrow A\right)\\
{\color{greenunder}\text{rule for parameterized types}:}\quad & ={\cal CH}\left(\forall A.\,A\rightarrow A\right)\quad.
\end{align*}
The last line shows the ${\cal CH}$-proposition that corresponds
to the function type $\forall A.\,A\rightarrow A$. Translating the
type notation into a Scala type signature, we get
\begin{lstlisting}
def f[A]: A => A
\end{lstlisting}
This type signature can be easily implemented,
\begin{lstlisting}
def f[A]: A => A = { x => x }
\end{lstlisting}
So, in this example we see how we converted a true formula in logic
into the type of a value \lstinline!f!, and we found that the function
\lstinline!f! can be implemented in code.

While the formula $\forall\alpha.\,\alpha=\alpha$ may be self-evident,
the point of using formal logic is to have a set of axioms and proof
rules that allow us to deduce \emph{all} correct formulas systematically,
without need for intuition or guessing. What axioms and proof rules
are suitable for proving ${\cal CH}$-propositions?

A well-known set of logical rules is called \index{Boolean logic}Boolean
logic. In that logic, each proposition is either $True$ or $False$,
and the implication operation ($\Rightarrow$) is \emph{defined} by
\begin{equation}
\left(\alpha\Rightarrow\beta\right)\triangleq\left((\neg\alpha)\vee\beta\right)\quad.\label{eq:ch-definition-of-implication-in-Boolean-logic}
\end{equation}
To verify a formula, substitute $True$ or $False$ into every variable
and check if the formula has the value $True$ in all possible cases.
The result can be arranged into a \index{truth table}truth table.
The basic operations (disjunction, conjunction, negation, and implication)
have the following truth tables:
\begin{center}
{\small{}}%
\begin{tabular}{|c|c|c|c|c|c|}
\hline 
{\small{}$\alpha$} & {\small{}$\beta$} & \textbf{\small{}$\alpha\vee\beta$} & \textbf{\small{}$\alpha\wedge\beta$} & \textbf{\small{}$\neg\alpha$} & \textbf{\small{}$\alpha\Rightarrow\beta$}\tabularnewline
\hline 
\hline 
{\small{}$True$} & {\small{}$True$} & {\small{}$True$} & {\small{}$True$} & {\small{}$False$} & {\small{}$True$}\tabularnewline
\hline 
{\small{}$True$} & {\small{}$False$} & {\small{}$True$} & {\small{}$False$} & {\small{}$False$} & {\small{}$False$}\tabularnewline
\hline 
{\small{}$False$} & {\small{}$True$} & {\small{}$True$} & {\small{}$False$} & {\small{}$True$} & {\small{}$True$}\tabularnewline
\hline 
{\small{}$False$} & {\small{}$False$} & {\small{}$False$} & {\small{}$False$} & {\small{}$True$} & {\small{}$True$}\tabularnewline
\hline 
\end{tabular}{\small\par}
\par\end{center}

The formula $\alpha\Rightarrow\alpha$ has the value $True$ whether
$\alpha$ itself is $True$ or $False$. This check is sufficient
to show that $\forall\alpha.\,\alpha\Rightarrow\alpha$ is true in
Boolean logic.

Here is the truth table for the formula $\forall(\alpha,\beta).\,(\alpha\wedge\beta)\Rightarrow\alpha$.
This formula is true in Boolean logic since all values in the last
column are $True$:
\begin{center}
{\small{}}%
\begin{tabular}{|c|c|c|c|}
\hline 
{\small{}$\alpha$} & {\small{}$\beta$} & \textbf{\small{}$\alpha\wedge\beta$} & {\small{}$(\alpha\wedge\beta)\Rightarrow\alpha$}\tabularnewline
\hline 
\hline 
{\small{}$True$} & {\small{}$True$} & {\small{}$True$} & {\small{}$True$}\tabularnewline
\hline 
{\small{}$True$} & {\small{}$False$} & {\small{}$False$} & {\small{}$True$}\tabularnewline
\hline 
{\small{}$False$} & {\small{}$True$} & {\small{}$False$} & {\small{}$True$}\tabularnewline
\hline 
{\small{}$False$} & {\small{}$False$} & {\small{}$False$} & {\small{}$True$}\tabularnewline
\hline 
\end{tabular}{\small\par}
\par\end{center}

The formula $\forall(\alpha,\beta).\,\alpha\Rightarrow(\alpha\wedge\beta)$
is not true in Boolean logic, which we can see from the following
truth table (one value in the last column is $False$):
\begin{center}
{\small{}}%
\begin{tabular}{|c|c|c|c|}
\hline 
{\small{}$\alpha$} & {\small{}$\beta$} & \textbf{\small{}$\alpha\wedge\beta$} & {\small{}$\alpha\Rightarrow(\alpha\wedge\beta)$}\tabularnewline
\hline 
\hline 
{\small{}$True$} & {\small{}$True$} & {\small{}$True$} & {\small{}$True$}\tabularnewline
\hline 
{\small{}$True$} & {\small{}$False$} & {\small{}$False$} & {\small{}$False$}\tabularnewline
\hline 
{\small{}$False$} & {\small{}$True$} & {\small{}$False$} & {\small{}$True$}\tabularnewline
\hline 
{\small{}$False$} & {\small{}$False$} & {\small{}$False$} & {\small{}$True$}\tabularnewline
\hline 
\end{tabular}{\small\par}
\par\end{center}

Table~\ref{tab:Logical-formulas-Boolean-theorems} shows more examples
of logical formulas that are true in Boolean logic. Each formula is
first given in terms of ${\cal CH}$-propositions (we denoted $\alpha\triangleq{\cal CH}(A)$
and $\beta\triangleq{\cal CH}(B)$ for brevity) and then into a Scala
type signature of a function that can be implemented.

\begin{table}
\begin{centering}
\begin{tabular}{|c|c|c|}
\hline 
\textbf{\small{}Logic formula} & \textbf{\small{}Type formula} & \textbf{\small{}Scala code}\tabularnewline
\hline 
\hline 
{\footnotesize{}$\forall\alpha.\,\alpha\Rightarrow\alpha$} & {\footnotesize{}$\forall A.\,A\rightarrow A$} & \lstinline!def id[A](x: A): A = x!\tabularnewline
\hline 
{\footnotesize{}$\forall\alpha.\,\alpha\Rightarrow True$} & {\footnotesize{}$\forall A.\,A\rightarrow\bbnum 1$} & \lstinline!def toUnit[A](x: A): Unit = ()!\tabularnewline
\hline 
{\footnotesize{}$\forall(\alpha,\beta).\,\alpha\Rightarrow(\alpha\vee\beta)$} & {\footnotesize{}$\forall(A,B).\,A\rightarrow A+B$} & \lstinline!def toL[A, B](x: A): Either[A, B] = Left(x)!\tabularnewline
\hline 
{\footnotesize{}$\forall(\alpha,\beta).\,(\alpha\wedge\beta)\Rightarrow\alpha$} & {\footnotesize{}$\forall(A,B).\,A\times B\rightarrow A$} & \lstinline!def first[A, B](p: (A, B)): A = p._1!\tabularnewline
\hline 
{\footnotesize{}$\forall(\alpha,\beta).\,\alpha\Rightarrow(\beta\Rightarrow\alpha)$} & {\footnotesize{}$\forall(A,B).\,A\rightarrow(B\rightarrow A)$} & \lstinline!def const[A, B](x: A): B => A = (_ => x)!\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{Examples of logical formulas that are true theorems in Boolean logic.\label{tab:Logical-formulas-Boolean-theorems}}
\end{table}

Table~\ref{tab:Logical-formulas-not-Boolean-theorems} some examples
of formulas that are \emph{not true} in Boolean logic. Translated
into type formulas and then into Scala, these formulas yield type
signatures that \emph{cannot} be implemented by fully parametric functions.

\begin{table}
\begin{centering}
\begin{tabular}{|c|c|c|}
\hline 
\textbf{\small{}Logic formula} & \textbf{\small{}Type formula} & \textbf{\small{}Scala type signature}\tabularnewline
\hline 
\hline 
{\footnotesize{}$\forall\alpha.\,True\Rightarrow\alpha$} & {\footnotesize{}$\forall A.\,\bbnum 1\rightarrow A$} & \lstinline!def f[A](x: Unit): A!\tabularnewline
\hline 
{\footnotesize{}$\forall(\alpha,\beta).\,(\alpha\vee\beta)\Rightarrow\alpha$} & {\footnotesize{}$\forall(A,B).\,A+B\rightarrow A$} & \lstinline!def f[A,B](x: Either[A, B])!\tabularnewline
\hline 
{\footnotesize{}$\forall(\alpha,\beta).\,\alpha\Rightarrow(\alpha\wedge\beta)$} & {\footnotesize{}$\forall(A,B).\,A\rightarrow A\times B$} & \lstinline!def f[A,B](p: A): (A, B)!\tabularnewline
\hline 
{\footnotesize{}$\forall(\alpha,\beta).\,(\alpha\Rightarrow\beta)\Rightarrow\alpha$} & {\footnotesize{}$\forall(A,B).\,(A\rightarrow B)\rightarrow A$} & \lstinline!def f[A,B](x: A => B): A!\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{Examples of logical formulas that are \emph{not} true in Boolean logic.\label{tab:Logical-formulas-not-Boolean-theorems}}
\end{table}

At first sight, it appears from these examples that whenever a logical
formula is true in Boolean logic, the corresponding type signature
can be implemented in code, and vice versa. However, this is \emph{incorrect}:
the rules of Boolean logic are not suitable for reasoning about types
in a functional language. Below we will see some examples of formulas
that are true in Boolean logic but correspond to unimplementable type
signatures.

\subsection{Example: Failure of Boolean logic when reasoning about $\mathcal{CH}$-propositions\label{subsec:Example:-Failure-of-Boolean-logic}}

Using Boolean logic to reason about values computed by fully parametric
functions may give incorrect results. To see that, consider the following
type:
\begin{equation}
\forall(A,B,C).\,\left(A\rightarrow B+C\right)\rightarrow\left(A\rightarrow B\right)+\left(A\rightarrow C\right)\quad,\label{eq:ch-example-boolean-bad-type}
\end{equation}
which corresponds to the Scala type signature
\begin{lstlisting}
def bad[A, B, C](g: A => Either[B, C]): Either[A => B, A => C] = ???
\end{lstlisting}
The function \lstinline!bad! \emph{cannot} be implemented via fully
parametric code. To see why, consider that the only available data
is a function $g^{:A\rightarrow B+C}$, which returns values of type
$B$ or $C$ depending (in some unknown way) on the input value of
type $A$. The function \lstinline!bad! must return either a function
of type $A\rightarrow B$ or a function of type $A\rightarrow C$.
How can the code of \lstinline!bad! make that decision? The only
input data is the function $g$ that takes an argument of type $A$.
We could imagine applying $g$ to various arguments of type $A$ and
to see whether $g$ returns a $B$ or a $C$. However, the type $A$
is arbitrary, and a fully parametric function cannot produce a value
of type $A$ in order to apply $g$ to it. So the decision about whether
to return $A\rightarrow B$ or $A\rightarrow C$ must be independent
of $g$; that decision must be hard-coded in the function \lstinline!bad!.

Suppose we hard-coded the decision to return a function of type $A\rightarrow B$.
How would we create a function of type $A\rightarrow B$ in the body
of \lstinline!bad!? Given a value $x^{:A}$ of type $A$, we would
need to compute some value of type $B$. Since the type $B$ is arbitrary
(it is a type parameter), we cannot produce a value of type $B$ from
scratch. The only potential source of values of type $B$ is the given
function $g$. The only way of using $g$ is to apply it to $x^{:A}$.
However, for some $x$, the value $g(x)$ may be of the form \lstinline!Right(c)!,
where \lstinline!c! is of type $C$. In that case, we will have a
value of type $C$, not $B$. So, in general, we cannot guarantee
that we can always obtain a value of type $B$ from a given value
$x^{:A}$. This means we cannot build a function of type $A\rightarrow B$
out of the function $g$. Similarly, we cannot build a function of
type $A\rightarrow C$ out of $g$. 

Whether we decide to return $A\rightarrow B$ or $A\rightarrow C$,
we will not be able to return a value of the required type, as we
just saw. We must conclude that we cannot implement \lstinline!bad!
as a fully parametric function.

We could try to switch between $A\rightarrow B$ and $A\rightarrow C$
depending on a given value of type $A$. This idea, however, means
that we are working with a different type signature: 
\[
\forall(A,B,C).\,\left(A\rightarrow B+C\right)\rightarrow A\rightarrow\left(A\rightarrow B\right)+\left(A\rightarrow C\right)\quad.
\]
This type signature \emph{can} be implemented, for instance, by this
Scala code:
\begin{lstlisting}
def q[A, B, C](g: A => Either[B, C]): A => Either[A => B, A => C] = { a =>
  g(a) match {
    case Left(b) => Left(_ => b)
    case Right(c) => Right(_ => c)
  }
}
\end{lstlisting}
But this is not the required type signature~(\ref{eq:ch-example-boolean-bad-type}).

Now let us convert the type signature~(\ref{eq:ch-example-boolean-bad-type})
into a ${\cal CH}$-proposition:
\begin{align}
 & \forall(\alpha,\beta,\gamma).\,\left(\alpha\Rightarrow\left(\beta\vee\gamma\right)\right)\Rightarrow\left(\left(\alpha\Rightarrow\beta\right)\vee\left(\alpha\Rightarrow\gamma\right)\right)\quad,\label{eq:abc-example-classical-logic-bad}\\
\text{where we denoted}\quad & \alpha\triangleq{\cal CH}(A),\quad\beta\triangleq{\cal CH}(B),\quad\gamma\triangleq{\cal CH}(C)\quad.\nonumber 
\end{align}
It turns out that this formula is true in Boolean logic. To prove
this, we need to show that Eq.~(\ref{eq:abc-example-classical-logic-bad})
is equal to $True$ for any Boolean values of the variables $\alpha$,
$\beta$, $\gamma$. One way is to rewrite the expression~(\ref{eq:abc-example-classical-logic-bad})
using the rules of Boolean logic, such as Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic}):
\begin{align*}
 & \gunderline{\alpha\Rightarrow}\left(\beta\vee\gamma\right)\\
{\color{greenunder}\text{definition of }\Rightarrow\text{ via Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & \quad=(\neg\alpha)\vee\beta\vee\gamma\quad,\\
 & \gunderline{\left(\alpha\Rightarrow\beta\right)}\vee\gunderline{\left(\alpha\Rightarrow\gamma\right)}\\
{\color{greenunder}\text{definition of }\Rightarrow\text{ via Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & \quad=\gunderline{(\neg\alpha)}\vee\beta\vee\gunderline{(\neg\alpha)}\vee\gamma\\
{\color{greenunder}\text{property }x\vee x=x\text{ in Boolean logic}:}\quad & \quad=(\neg\alpha)\vee\beta\vee\gamma\quad,
\end{align*}
showing that $\alpha\Rightarrow(\beta\vee\gamma)$ is in fact \emph{equal}
to $\left(\alpha\Rightarrow\beta\right)\vee\left(\alpha\Rightarrow\gamma\right)$
in Boolean logic.

Let us also give a proof via truth-value reasoning. The only possibility
for an implication $X\Rightarrow Y$ to be $False$ is when $X=True$
and $Y=False$. So, Eq.~(\ref{eq:abc-example-classical-logic-bad})
can be $False$ only if $\left(\alpha\Rightarrow(\beta\vee\gamma)\right)=True$
and $\left(\alpha\Rightarrow\beta\right)\vee\left(\alpha\Rightarrow\gamma\right)=False$.
A disjunction can be false only when both parts are false; so we must
have both $\left(\alpha\Rightarrow\beta\right)=False$ and $\left(\alpha\Rightarrow\gamma\right)=False$.
This is only possible if $\alpha=True$ and $\beta=\gamma=False$.
But, with these value assignments, we find $\left(\alpha\Rightarrow(\beta\vee\gamma)\right)=False$
rather than $True$ as we assumed. It follows that we cannot ever
make Eq.~(\ref{eq:abc-example-classical-logic-bad}) equal to $False$.
So, Eq.~(\ref{eq:abc-example-classical-logic-bad}) is true in Boolean
logic.

\subsection{The rules of proof for ${\cal CH}$-propositions\label{subsec:The-rules-of-proof}}

Section~\ref{subsec:Example:-Failure-of-Boolean-logic} shows that
some true formulas in Boolean logic do not correspond to types of
\emph{implementable} fully parametric functions. However, we have
also seen several other examples where Boolean logic does provide
correct results: some true formulas correspond to implementable type
signatures, while some false formulas correspond to non-implementable
type signatures.

Instead of guessing whether the rules of Boolean logic are suitable
in a given case, let us derive the suitable logical axioms and proof
rules systematically.

The proposition ${\cal CH}(A)$ is true when a value of type $A$
can be computed by a fully parametric function with a given type signature.
To describe all possible ways of computing a value of type $A$, we
need to enumerate all possible ways of \emph{writing code} within
a fully parametric function. The requirement of parametricity means
that we are not allowed to use any specific types such as \lstinline!Int!
or \lstinline!String!, any concrete values such as \lstinline!123!
or \lstinline!"hello"!, or any library functions that work with specific
(non-parametric) types. We are only allowed to work with values of
unknown types described by the given type parameters. However, we
are permitted to use fully parametric types such as \lstinline!Either[A, B]!
or \lstinline!Option[A]!. The allowed eight code constructions\index{eight code constructions}
are illustrated in this code fragment:
\begin{lstlisting}
def f[A, B, ...](a: A, b: B)... = {   // Any given type signature.
  val x1: Unit = ()                   // 1) Use a value of type Unit.
  val x2: A = a                       // 2) Use a given argument.
  val x3 = { x: A => ... }            // 3) Create a function.
  val x4: D = x3(x2)                  // 4) Use a function.
  val x5: (A, B) = (a, b)             // 5) Create a tuple.
  val x6: B = x5._2                   // 6) Use a tuple.
  val x7: Option[A] = Some(x2)        // 7) Create values of a disjunctive type.
  val x8 = x7 match { ... }           // 8) Use values of a disjunctive type.
}     // 9) Call f() itself recursively. Not included here because CH-propositions do not support it.
\end{lstlisting}
A value of type $X$ can be computed (i.e., ${\cal CH}(X)$ is true)
if and only if we can create a sequence of computed values such as
\lstinline!x1!, \lstinline!x2!, ..., each being the result of one
of these eight code constructs, ending with a value of type $X$.
So, each of the eight code constructs should correspond to one of
the logical rules for proving a ${\cal CH}$-proposition.

A set of proof rules defines a \textbf{formal logic}\index{formal logic}.
There is a specific formal logic that gives correct answers when reasoning
about ${\cal CH}$-propositions. The proof rules of that logic are
found by translating the eight code constructs into sequents. A proof
of a sequent, e.g., $\mathcal{CH}(A)\vdash\mathcal{CH}(X)$, must
consist of applying some of those proof rules. We will then combine
the code constructs corresponding to each rule and obtain some code
that computes a value of type $X$ using an argument of type $A$.
Conversely, any fully parametric (and non-recursive) code computing
a value of type $X$ must be a combination of some of the eight code
constructs\index{eight code constructions}. That code combination
can be automatically translated into a combination of logic rules,
in order to produce a proof of the proposition ${\cal CH}(X)$.

In the following sections, we will need to consider the full formulation~(\ref{eq:ch-CH-proposition-def})
of ${\cal CH}$-propositions and write them as sequents such as Eq.~(\ref{eq:ch-example-sequent}).
For brevity, we define $\alpha\triangleq{\cal CH}(A)$, $\beta\triangleq{\cal CH}(B)$,
etc. It is also customary to use the letter $\Gamma$ to denote a
set of premises, such as ${\cal CH}(X)$, ${\cal CH}(Y)$, ..., ${\cal CH}(Z)$
in Eq.~(\ref{eq:ch-example-sequent}). So, we can write a shorter
formula $\Gamma\vdash\alpha$ instead of the sequent~(\ref{eq:ch-example-sequent}).

With these notations, we now enumerate the rules for proving ${\cal CH}$-propositions. 

\paragraph{1) Use the \texttt{Unit} value}

At any place in the code, we may write the expression \lstinline!()!
of type \lstinline!Unit!. This expression corresponds to a proof
of the proposition ${\cal CH}(\bbnum 1)$ with any set $\Gamma$ of
premises (even with an empty set of premises). So, the sequent $\Gamma\vdash{\cal CH}(\bbnum 1)$
is always true. The code corresponding to the proof of this sequent
is an expression that creates a value of the \lstinline!Unit! type:
\[
\text{Proof}\,\big(\Gamma\vdash{\cal CH}(\bbnum 1)\big)=1\quad,
\]
where we denoted by $1$ the value \lstinline!()!.

In formal logic, a sequent that is found to be always true, such as
our $\Gamma\vdash{\cal CH}(\bbnum 1)$, is called an \textbf{axiom}\index{logical axiom}
and is written in the following notation,
\[
\frac{}{\Gamma\vdash{\cal CH}(\bbnum 1)}\quad(\text{create unit})\quad\quad.
\]
The \textsf{``}fraction with a label\textsf{''} represents a proof rule. The denominator
of the \textsf{``}fraction\textsf{''} is the target sequent that we need to prove.
The numerator of the \textsf{``}fraction\textsf{''} can have zero or more other sequents
that need to be proved before the target sequent can be proved. In
this case, the set of previous sequents is empty: the target sequent
is an axiom and so requires no previous sequents for its proof. The
label \textsf{``}$\text{create unit}$\textsf{''} is an arbitrary name used to refer
to the rule.

\paragraph{2) Use a given argument}

At any place within the code of a fully parametric function, we may
use one of the function\textsf{'}s arguments, say $x^{:A}$. If some argument
has type $A$, it means that $\alpha\triangleq{\cal CH}(A)$ belongs
to the set of premises of the sequent we are trying to prove. To indicate
this, we write the set of premises as \textsf{``}$\Gamma,\alpha$\textsf{''}. The
code construct \lstinline!x:A! computes a value of type $A$, i.e.,
show that $\alpha$ is true, given these premises. This is expressed
by the sequent $\Gamma,\alpha\vdash\alpha$. The proof of this sequent
corresponds to an expression that returns one of the given arguments
(which we here called $x^{:A}$),
\[
\text{Proof}\,\big(\Gamma,\alpha\vdash\alpha\big)=x^{:A}\quad.
\]
This sequent is an axiom since its proof requires no previous sequents.
The formal logic notation for this axiom is
\[
\frac{~}{\Gamma,\alpha\vdash\alpha}\quad(\text{use arg})\quad\quad.
\]


\paragraph{3) Create a function}

At any place in the code, we may compute a nameless function of type,
say, $A\rightarrow B$, by writing \lstinline!(x:A) => expr! as long
as a value \lstinline!expr! of type $B$ can be computed in the inner
scope of the function. The code for \lstinline!expr! is also required
to be fully parametric; it may use \lstinline!x! and/or other values
visible in that scope. So we now need to answer the question of whether
a fully parametric function can compute a value of type $B$, given
an argument of type $A$ as well as all other arguments previously
given to the parent function. This question is answered by a sequent
whose premises contain one more proposition, ${\cal CH}(A)$, in addition
to all previously available premises. Translating this into the language
of ${\cal CH}$-propositions, we find that we will prove the sequent
\[
\Gamma\vdash{\cal CH}(A\rightarrow B)\quad=\quad\Gamma\vdash{\cal CH}(A)\Rightarrow{\cal CH}(B)\quad\triangleq\quad\Gamma\vdash\alpha\Rightarrow\beta
\]
if we can prove the sequent $\Gamma,{\cal CH}(A)\vdash{\cal CH}(B)=\Gamma,\alpha\vdash\beta$.
In the notation of formal logic, this is a \textbf{derivation rule}\index{derivation rule}
(rather than an axiom) and is written as
\[
\frac{\Gamma,\alpha\vdash\beta}{\Gamma\vdash\alpha\Rightarrow\beta}\quad(\text{create function})\quad\quad.
\]
The \textbf{turnstile}\index{turnstile symbol} symbol, $\vdash$,
groups weaker than other operators. So, we can write sequents such
as $(\Gamma,\alpha)\vdash(\beta\Rightarrow\gamma)$ with fewer parentheses:
$\Gamma,\alpha\vdash\beta\Rightarrow\gamma$.

What code corresponds to the \textsf{``}$\text{create function}$\textsf{''} rule?
The proof of $\Gamma\vdash\alpha\Rightarrow\beta$ depends on a proof
of another sequent. So, the corresponding code must be a \emph{function}
that takes a proof of the previous sequent as an argument and returns
a proof of the new sequent. By the CH correspondence, a proof of a
sequent corresponds to a code expression of the type given by the
goal of the sequent; the expression may use arguments of types corresponding
to the premises of the sequent. So, a proof of the sequent $\Gamma,\alpha\vdash\beta$
is an expression \lstinline!exprB! of type $B$ that may use a given
value of type $A$ as well as any other arguments given previously.
Then we can write the proof code for the sequent $\Gamma\vdash\alpha\Rightarrow\beta$
as the nameless function \lstinline!(x:A) => exprB!. This function
has type $A\rightarrow B$ and requires us to already have a suitable
\lstinline!exprB!. This exactly corresponds to the proof rule \textsf{``}$\text{create function}$\textsf{''}.
We may write the corresponding code as
\[
\text{Proof}\,\big(\Gamma\vdash{\cal CH}(A)\Rightarrow{\cal CH}(B)\big)=x^{:A}\rightarrow\text{Proof}\,\big(\Gamma,x^{:A}\vdash{\cal CH}(B)\big)\quad.
\]
Here we wrote $x^{:A}$ instead of ${\cal CH}(A)$ since the value
$x^{:A}$ is a proof of the proposition ${\cal CH}(A)$. We will see
in Section~\ref{subsec:Example:-Proving-a-ch-proposition} how premises
such as $\Gamma,x^{:A}$ are implemented in code.

\paragraph{4) Use a function}

At any place in the code, we may apply an already defined function
of type $A\rightarrow B$ to an already computed value of type $A$.
The result will be a value of type $B$. This corresponds to assuming
${\cal CH}(A\rightarrow B)$ and ${\cal CH}(A)$, and then deriving
${\cal CH}(B)$. The formal logic notation for this proof rule is
\[
\frac{\Gamma\vdash\alpha\quad\quad\Gamma\vdash\alpha\Rightarrow\beta}{\Gamma\vdash\beta}\quad(\text{use function})\quad\quad.
\]
The code corresponding to this proof rule takes previously computed
values \lstinline!x:A! and \lstinline!f:A => B!, and writes the
expression \lstinline!f(x)!. This can be written as a function application,
\[
\text{Proof}\,(\Gamma\vdash\beta)=\text{Proof}\left(\Gamma\vdash\alpha\Rightarrow\beta\right)(\text{Proof}\,(\Gamma\vdash\alpha))\quad.
\]


\paragraph{5) Create a tuple}

If we have already computed some values \lstinline!a:A! and \lstinline!b:B!,
we may write the expression \lstinline!(a, b)! and so compute a value
of the tuple type \lstinline!(A, B)!. The proof rule is
\[
\frac{\Gamma\vdash\alpha\quad\quad\Gamma\vdash\beta}{\Gamma\vdash\alpha\wedge\beta}\quad(\text{create tuple})\quad\quad.
\]
Writing $a\times b$ to mean the pair \lstinline!(a, b)!, we can
write the corresponding code expression as
\[
\text{Proof}\left(\Gamma\vdash\alpha\wedge\beta\right)=\text{Proof}\left(\Gamma\vdash\alpha\right)\times\text{Proof}\left(\Gamma\vdash\beta\right)\quad.
\]

This rule describes creating a tuple of $2$ values. A larger tuple,
such as \lstinline!(w, x, y, z)!, can be expressed via nested pairs,
e.g., as \lstinline!(w, (x, (y, z)))!. So, it suffices to have a
sequent rule for creating pairs; this rule can express the sequent
rules for creating all other tuples, and we do not need to define
separate rules for, say, $\Gamma\vdash\alpha\wedge\beta\wedge\gamma$.

\paragraph{6) Use a tuple}

If we already have a value \lstinline!t:(A,B)! of a tuple type $A\times B$,
we can extract one of the parts of the tuple and obtain a value of
type \lstinline!A! or a value of type \lstinline!B!. The code is
\lstinline!t._1! and \lstinline!t._2! respectively, and the corresponding
sequent proof rules are
\[
\frac{\Gamma\vdash\alpha\wedge\beta}{\Gamma\vdash\alpha}\quad(\text{use tuple-}1)\quad\quad\quad\frac{\Gamma\vdash\alpha\wedge\beta}{\Gamma\vdash\beta}\quad(\text{use tuple-}2)\quad\quad.
\]
The code can be written as
\begin{align*}
\text{Proof}\left(\Gamma\vdash\alpha\right) & =\pi_{1}\left(\text{Proof}\left(\Gamma\vdash\alpha\wedge\beta\right)\right)\quad,\\
\text{Proof}\left(\Gamma\vdash\beta\right) & =\pi_{2}\left(\text{Proof}\left(\Gamma\vdash\alpha\wedge\beta\right)\right)\quad,
\end{align*}
where we introduced the notation $\pi_{1}$ and $\pi_{2}$ to mean
the Scala code \lstinline!_._1! and \lstinline!_._2!.

Since all tuples can be expressed through pairs, it is sufficient
to have proof rules for pairs.

\paragraph{7) Create a disjunctive value}

The type \lstinline!Either[A, B]! corresponding to the disjunction
$\alpha\vee\beta$ can be used to define any other disjunctive type;
e.g., a disjunctive type with three parts can be expressed as \lstinline!Either[A, Either[B, C]]!.
So it is sufficient to have proof rules for a disjunction of \emph{two}
propositions.

There are two ways of creating a value of the type \lstinline!Either[A, B]!:
the code expressions are \lstinline!Left(x:A)! and \lstinline!Right(y:B)!.
The values \lstinline!x:A! or \lstinline!y:B! must have been computed
previously (and correspond to previously proved sequents). So, the
sequent proof rules are
\[
\frac{\Gamma\vdash\alpha}{\Gamma\vdash\alpha\vee\beta}\quad(\text{create Left})\quad\quad\quad\frac{\Gamma\vdash\beta}{\Gamma\vdash\alpha\vee\beta}\quad(\text{create Right})\quad\quad.
\]
The corresponding code can be written using the case class names \lstinline!Left!
and \lstinline!Right! as 
\begin{align*}
\text{Proof}\left(\Gamma\vdash\alpha\vee\beta\right) & =\text{Left}\,(\text{Proof}\left(\Gamma\vdash\alpha\right))\quad,\\
\text{Proof}\left(\Gamma\vdash\alpha\vee\beta\right) & =\text{Right}\,(\text{Proof}\left(\Gamma\vdash\beta\right))\quad.
\end{align*}


\paragraph{8) Use a disjunctive value}

The basic way of using a value of the disjunctive type \lstinline!Either[A, B]!
is by pattern matching on it:

\begin{wrapfigure}{l}{0.43\columnwidth}%
\vspace{-0.6\baselineskip}
\begin{lstlisting}
val result: C = (e: Either[A, B]) match {
  case Left(x:A)    => expr1(x)
  case Right(y:B)   => expr2(y)
}
\end{lstlisting}

\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent Here, \lstinline!expr1(x)! must be an expression of some
type \lstinline!C!, computed using \lstinline!x:A! and any previously
available arguments (i.e., the premises $\Gamma$). Similarly, \lstinline!expr2(y)!
must be an expression of type \lstinline!C! computed using \lstinline!y:B!
and previous arguments. It is clear that \lstinline!expr1(x)! represents
a proof of a sequent with an additional premise of type \lstinline!A!,
i.e., $\Gamma,\alpha\vdash\gamma$, where we denoted $\gamma\triangleq{\cal CH}(C)$.
Similarly, \lstinline!expr2(y)! is a proof of the sequent $\Gamma,\beta\vdash\gamma$.
So, we can write the proof rule corresponding to the \lstinline!match!/\lstinline!case!
expression as a rule with three previous sequents:
\[
\frac{\Gamma\vdash\alpha\vee\beta\quad\quad\Gamma,\alpha\vdash\gamma\quad\quad\Gamma,\beta\vdash\gamma}{\Gamma\vdash\gamma}\quad(\text{use Either})\quad\quad.
\]
The code can be written as
\[
\text{Proof}\left(\Gamma\vdash\gamma\right)=\text{Proof}\left(\Gamma\vdash\alpha\vee\beta\right)\text{ match }\begin{cases}
\text{case }a^{:A}\rightarrow & \bbnum 0^{:B}+a^{:A}\\
\text{case }b^{:B}\rightarrow & b^{:B}+\bbnum 0^{:A}
\end{cases}\quad.
\]

Table~\ref{tab:Proof-rules-for-constructive-logic} summarizes the
eight proof rules derived in this section. These proof rules define
a logic known as the \textbf{\index{intuitionistic propositional logic}intuitionistic
propositional logic} or \textbf{\index{constructive logic}constructive
propositional logic}. We will call this logic \textsf{``}constructive\textsf{''} for
short.

\begin{table}
\begin{centering}
{\small{}}%
\fbox{\begin{minipage}[t]{0.75\columnwidth}%
{\small{}
\begin{align*}
{\color{greenunder}\text{axioms}:}\quad & \frac{~}{\Gamma\vdash{\cal CH}(\bbnum 1)}\quad(\text{use unit})\quad\quad\quad\quad\frac{~}{\Gamma,\alpha\vdash\alpha}\quad(\text{use arg})\\
{\color{greenunder}\text{derivation rules}:}\quad & \frac{\Gamma,\alpha\vdash\beta}{\Gamma\vdash\alpha\Rightarrow\beta}\quad(\text{create function})\\
 & \frac{\Gamma\vdash\alpha\quad\quad\Gamma\vdash\alpha\Rightarrow\beta}{\Gamma\vdash\beta}\quad(\text{use function})\\
 & \frac{\Gamma\vdash\alpha\quad\quad\Gamma\vdash\beta}{\Gamma\vdash\alpha\wedge\beta}\quad(\text{create tuple})\\
 & \frac{\Gamma\vdash\alpha\wedge\beta}{\Gamma\vdash\alpha}\quad(\text{use tuple-}1)\quad\quad\quad\frac{\Gamma\vdash\alpha\wedge\beta}{\Gamma\vdash\beta}\quad(\text{use tuple-}2)\\
 & \frac{\Gamma\vdash\alpha}{\Gamma\vdash\alpha\vee\beta}\quad(\text{create \texttt{Left}})\quad\quad\quad\frac{\Gamma\vdash\beta}{\Gamma\vdash\alpha\vee\beta}\quad(\text{create \texttt{Right}})\\
 & \frac{\Gamma\vdash\alpha\vee\beta\quad\quad\Gamma,\alpha\vdash\gamma\quad\quad\Gamma,\beta\vdash\gamma}{\Gamma\vdash\gamma}\quad(\text{use \texttt{Either}})
\end{align*}
}%
\end{minipage}}{\small\par}
\par\end{centering}
\caption{Proof rules for the constructive logic.\label{tab:Proof-rules-for-constructive-logic}}
\end{table}


\subsection{Example: Proving a ${\cal CH}$-proposition and deriving code\label{subsec:Example:-Proving-a-ch-proposition}}

The task is to implement a fully parametric function

\begin{wrapfigure}{l}{0.45\columnwidth}%
\vspace{-0.75\baselineskip}
\begin{lstlisting}
def f[A, B]: ((A => A) => B) => B = ???
\end{lstlisting}

\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent Implementing this function is the same as being able to
compute a value of type $F$, where $F$ is defined as
\[
F\triangleq\forall(A,B).\,((A\rightarrow A)\rightarrow B)\rightarrow B\quad.
\]
Since the type parameters $A$ and $B$ are arbitrary, the body of
the fully parametric function \lstinline!f! cannot use any previously
defined values of types $A$ or $B$. So, the task is formulated as
computing a value of type $F$ with \emph{no} previously defined values.
This is written as the sequent $\Gamma\vdash{\cal CH}(F)$, where
the set $\Gamma$ of premises is empty, $\Gamma=\emptyset$. Rewriting
this sequent using the rules of Table~\ref{tab:ch-correspondence-type-notation-CH-propositions},
we get
\begin{equation}
\forall(\alpha,\beta).~\emptyset\vdash((\alpha\Rightarrow\alpha)\Rightarrow\beta)\Rightarrow\beta\quad,\label{eq:ch-example-sequent-2}
\end{equation}
where we denoted $\alpha\triangleq{\cal CH}(A)$ and $\beta\triangleq{\cal CH}(B)$. 

The next step is to prove the sequent~(\ref{eq:ch-example-sequent-2})
using the proof rules of Section~\ref{subsec:The-rules-of-proof}.
For brevity, we will omit the quantifier $\forall(\alpha,\beta)$
since it will be present in front of every sequent.

Begin by looking for a proof rule whose \textsf{``}denominator\textsf{''} has a sequent
similar to Eq.~(\ref{eq:ch-example-sequent-2}), i.e., has an implication
($p\Rightarrow q$) in the goal. We have only one rule that can prove
a sequent of the form $\Gamma\vdash(p\Rightarrow q$); this is the
rule \textsf{``}$\text{create function}$\textsf{''}. That rule requires us to already
have a proof of the sequent $(\Gamma,p)\vdash q$. So, we use this
rule with $\Gamma=\emptyset$, and we set $p\triangleq(\alpha\Rightarrow\alpha)\Rightarrow\beta$
and $q\triangleq\beta$: 
\[
\frac{(\alpha\Rightarrow\alpha)\Rightarrow\beta\vdash\beta}{\emptyset\vdash((\alpha\Rightarrow\alpha)\Rightarrow\beta)\Rightarrow\beta}\quad.
\]
We now need to prove the sequent $(\alpha\Rightarrow\alpha)\Rightarrow\beta)\vdash\beta$,
which we can write as $\Gamma_{1}\vdash\beta$ where $\Gamma_{1}\triangleq[(\alpha\Rightarrow\alpha)\Rightarrow\beta]$
denotes the set containing the single premise $(\alpha\Rightarrow\alpha)\Rightarrow\beta$. 

There are no proof rules that derive a sequent with an explicit premise
of the form of an implication $p\Rightarrow q$. However, we have
a rule called \textsf{``}$\text{use function}$\textsf{''} that derives a sequent
by assuming another sequent containing an implication. We would be
able to use that rule,
\[
\frac{\Gamma_{1}\vdash\alpha\Rightarrow\alpha\quad\quad\Gamma_{1}\vdash(\alpha\Rightarrow\alpha)\Rightarrow\beta}{\Gamma_{1}\vdash\beta}\quad,
\]
if we could prove the two sequents $\Gamma_{1}\vdash\alpha\Rightarrow\alpha$
and $\Gamma_{1}\vdash(\alpha\Rightarrow\alpha)\Rightarrow\beta$.
To prove these sequents, note that the rule \textsf{``}$\text{create function}$\textsf{''}
applies to $\Gamma_{1}\vdash\alpha\Rightarrow\alpha$ like this,
\[
\frac{\Gamma_{1},\alpha\vdash\alpha}{\Gamma_{1}\vdash\alpha\Rightarrow\alpha}\quad.
\]
The sequent $\Gamma_{1},\alpha\vdash\alpha$ is proved directly by
the axiom \textsf{``}$\text{use arg}$\textsf{''}. The sequent $\Gamma_{1}\vdash(\alpha\Rightarrow\alpha)\Rightarrow\beta$
is also proved by the axiom \textsf{``}$\text{use arg}$\textsf{''} because $\Gamma_{1}$
already contains $(\alpha\Rightarrow\alpha)\Rightarrow\beta$.

The proof of the sequent~(\ref{eq:ch-example-sequent-2}) is now
complete and can be visualized as a tree (Figure~\ref{fig:Proof-of-the-sequent-example-2}).
The next step is to extract the code from that proof.

To do that, we combine the code expressions that correspond to each
of the proof rules we used. We need to retrace the proof backwards,
starting from the leaves of the tree and going towards the root. We
will then assemble the $\text{Proof}\left(...\right)$ code expressions
one by one.

\begin{figure}
\begin{centering}
{\footnotesize{}}%
\fbox{\begin{minipage}[t]{0.5\columnwidth}%
\begin{center}
{\footnotesize{}}{\footnotesize{}\Tree[ .$\emptyset\vdash((\alpha\Rightarrow\alpha)\Rightarrow\beta)\Rightarrow\beta $ [ .{rule \textsf{``}$\text{create function}$\textsf{''}} [ .$(\alpha\Rightarrow\alpha)\Rightarrow\beta\vdash\beta$ [ .{rule \textsf{``}$\text{use function}$\textsf{''}} [ .$(\alpha\Rightarrow\alpha)\Rightarrow\beta\vdash\alpha\Rightarrow\alpha$ [ .{rule \textsf{``}$\text{create function}$\textsf{''}} [ .$\Gamma_1,\alpha\vdash\alpha$ {axiom \textsf{``}$\text{use arg}$\textsf{''}} ] ] ] [ .$(\alpha\Rightarrow\alpha)\Rightarrow\beta\vdash(\alpha\Rightarrow\alpha)\Rightarrow\beta$ {axiom \textsf{``}$\text{use arg}$\textsf{''}} ] ] ] ] ]}
\par\end{center}%
\end{minipage}}{\footnotesize\par}
\par\end{centering}
\caption{Proof tree for sequent~(\ref{eq:ch-example-sequent-2}).\label{fig:Proof-of-the-sequent-example-2}}
\end{figure}

Begin with the left-most leaf \textsf{``}$\text{use arg}$\textsf{''}. This rule corresponds
to the code $x^{:A}$,
\[
\text{Proof}\left(\Gamma_{1},\alpha\vdash\alpha\right)=x^{:A}\quad.
\]
Here $x^{:A}$ must be a proof of the premise $\alpha$ in the sequent
$\Gamma_{1},\alpha\vdash\alpha$. So, we need to use the same $x^{:A}$
when we write the code for the previous rule, \textsf{``}$\text{create function}$\textsf{''}:
\[
\text{Proof}\left(\Gamma_{1}\vdash\alpha\Rightarrow\alpha\right)=(x^{:A}\rightarrow\text{Proof}\left(\Gamma_{1},\alpha\vdash\alpha\right))=(x^{:A}\rightarrow x)\quad.
\]
The right-most leaf \textsf{``}$\text{use arg}$\textsf{''} corresponds to the code
$f^{:(A\rightarrow A)\rightarrow B}$, where $f$ is the premise contained
in $\Gamma_{1}$. So we can write
\[
\text{Proof}\left(\Gamma_{1}\vdash(\alpha\Rightarrow\alpha)\Rightarrow\beta\right)=f^{:(A\rightarrow A)\rightarrow B}\quad.
\]
The previous rule, \textsf{``}$\text{use function}$\textsf{''}, combines the two
preceding proofs:
\begin{align*}
 & \text{Proof}\left((\alpha\Rightarrow\alpha)\Rightarrow\beta\vdash\beta\right)\\
 & =\text{Proof}\,(\Gamma_{1}\vdash(\alpha\Rightarrow\alpha)\Rightarrow\beta)\left(\text{Proof}\,(\Gamma_{1}\vdash\alpha\Rightarrow\alpha)\right)\\
 & =f(x^{:A}\rightarrow x)\quad.
\end{align*}
Going further backwards, we find that the rule applied before \textsf{``}$\text{use function}$\textsf{''}
was \textsf{``}$\text{create function}$\textsf{''}. We need to provide the same $f^{:\left(A\rightarrow A\right)\rightarrow B}$
as in the premise above, and so we obtain the code
\begin{align*}
 & \text{Proof}\left(\emptyset\vdash((\alpha\Rightarrow\alpha)\Rightarrow\beta)\Rightarrow\beta\right)\\
 & =f^{:\left(A\rightarrow A\right)\rightarrow B}\rightarrow\text{Proof}\left((\alpha\Rightarrow\alpha)\Rightarrow\beta\vdash\beta\right)\\
 & =f^{:\left(A\rightarrow A\right)\rightarrow B}\rightarrow f(x^{:A}\rightarrow x)\quad.
\end{align*}
This is the final code expression that implements the type $((A\rightarrow A)\rightarrow B)\rightarrow B$.
In this way, we have systematically derived the code from the type
signature of a function. That function can be written in Scala as
\begin{lstlisting}
def f[A, B]: ((A => A) => B) => B = { f => f(x => x) }
\end{lstlisting}

We found the proof tree in Figure~\ref{fig:Proof-of-the-sequent-example-2}
by guessing how to combine various proof rules. If we \emph{somehow}
find a proof tree for a sequent, we can prove the sequent and derive
the corresponding code. However, it is not always obvious how to combine
the proof rules to prove a given initial sequent. This is because
the rules of Table~\ref{tab:Proof-rules-of-constructive-and-boolean}
do not provide an algorithm for finding a proof tree automatically.
It turns out that such an algorithm exists (the \textsf{``}\index{LJT algorithm}LJT
algorithm\textsf{''}, see Appendix~\ref{app:CH-correspondence-LJT-algorithm}).
That algorithm can find proofs and infer code from type signatures
containing tuples, disjunctive types, and function types, if the given
type signature can be implemented.

The library \texttt{curryhoward}\footnote{\texttt{\href{https://github.com/Chymyst/curryhoward}{https://github.com/Chymyst/curryhoward}}}
implements the LJT algorithm. Here are some examples of using this
library for \textsf{``}\index{code inference}code inference\textsf{''}. We will run
the \texttt{ammonite}\footnote{\texttt{\href{http://ammonite.io/\#Ammonite-Shell}{http://ammonite.io/\#Ammonite-Shell}}}
shell to load the library more easily.

As a non-trivial (but artificial) example, consider the type signature
\[
\forall(A,B).\,\left(\left(\left(\left(A\rightarrow B\right)\rightarrow A\right)\rightarrow A\right)\rightarrow B\right)\rightarrow B\quad.
\]
It is not immediately clear whether it is possible to implement a
function with this type signature. It turns out that it \emph{is}
possible, and the code can be derived automatically by the LJT algorithm.
The library does this via the method \lstinline!implement!:
\begin{lstlisting}
@ import $ivy.`io.chymyst::curryhoward:0.3.7`, io.chymyst.ch._

@ def f[A, B]: ((((A => B) => A) => A) => B) => B   =   implement
defined function f

@ println(f.lambdaTerm.prettyPrint)
a => a (b => b (c => a (d => c)))
\end{lstlisting}
The code $a\rightarrow a\left(b\rightarrow b\left(c\rightarrow a\left(d\rightarrow c\right)\right)\right)$
was derived automatically for the function \lstinline!f!. The function
\lstinline!f! has been compiled and is ready to be used in any subsequent
code.

A compile-time error occurs when trying to use a type signature that
cannot be implemented as a fully parametric function:

\begin{wrapfigure}{l}{0.595\columnwidth}%
\vspace{-0.95\baselineskip}
\begin{lstlisting}
@ def g[A, B]: ((A => B) => A) => A   =   implement
cmd3.sc:1: type ((A => B) => A) => A cannot be implemented
def g[A, B]: ((A => B) => A) => A   =   implement
                                        ^
Compilation Failed
\end{lstlisting}

\vspace{-0.7\baselineskip}
\end{wrapfigure}%

\noindent The logical formula corresponding to this type signature
is \vspace{-0\baselineskip}
\begin{equation}
\forall(\alpha,\beta).\,\left(\left(\alpha\Rightarrow\beta\right)\Rightarrow\alpha\right)\Rightarrow\alpha\quad.\label{eq:ch-example-3-peirce-law}
\end{equation}
This formula is known as \textsf{``}Peirce\textsf{'}s law\textsf{''}.\footnote{\texttt{\href{https://en.wikipedia.org/wiki/Peirce\%27s_law}{https://en.wikipedia.org/wiki/Peirce\%27s\_law}}}
It is another example showing that the logic of types in functional
programming languages is not Boolean. Peirce\textsf{'}s law is a true theorem
in Boolean logic but does not hold in the constructive logic (i.e.,
it cannot be derived using the proof rules of Table~\ref{tab:Proof-rules-of-constructive-and-boolean}).
If we try to implement \lstinline!g[A, B]! with the type signature
shown above, we will fail to write fully parametric code for \lstinline!g!
that compiles without type errors. This is because no such code exists,
\textemdash{} not because we are insufficiently clever. The LJT algorithm
can \emph{prove} that the given type signature cannot be implemented;
the \texttt{curryhoward} library will then print an error message,
and compilation will fail.

As another example, let us verify that the type signature from Section~\ref{subsec:Example:-Failure-of-Boolean-logic}
is not implementable by fully parametric functions:
\begin{lstlisting}
@ def bad[A, B, C](g: A => Either[B, C]): Either[A => B, A => C]   =   implement
cmd4.sc:1: type (A => Either[B, C]) => Either[A => B, A => C] cannot be implemented
def bad[A, B, C](g: A => Either[B, C]): Either[A => B, A => C]   =   implement
                                                                     ^
Compilation Failed
\end{lstlisting}
The rules of constructive logic and the LJT algorithm define rigorously
what it means to infer code \textsf{``}guided by the types\textsf{''}. However, in
order to use the LJT algorithm productively, a programmer must know
how to infer code from types by hand. We will practice doing that
throughout the book.

\section{Solved examples: Equivalence of types}

We found a correspondence between types, code, logical propositions,
and proofs, which is known as the \textbf{Curry-Howard correspondence}\index{Curry-Howard correspondence}.
An example of the CH correspondence is that a proof of the logical
proposition
\begin{equation}
\forall(\alpha,\beta).\,\alpha\Rightarrow\left(\beta\Rightarrow\alpha\right)\label{eq:ch-proposition-example-2}
\end{equation}
corresponds to the code of the function 
\begin{lstlisting}
def f[A, B]: A => (B => A) = { x => _ => x }
\end{lstlisting}
With the CH correspondence in mind, we may say that the \emph{existence}
of the code \lstinline!x => _ => x! with the type $A\rightarrow(B\rightarrow A)$
\textsf{``}is\textsf{''} a proof of the logical formula~(\ref{eq:ch-proposition-example-2}),
because it shows how to compute a value of type $\forall(A,B).\,A\rightarrow B\rightarrow A$.

The Curry-Howard correspondence maps logic formulas such as $(\alpha\vee\beta)\wedge\gamma$
into type expressions such as $\left(A+B\right)\times C$. We have
seen that types behave similarly to logic formulas in one respect:
A logic formula is a true theorem of constructive logic when the corresponding
type signature can be implemented as a fully parametric function,
and vice versa.

It turns out that the similarity ends here. In other respects, type
expressions behave as \emph{arithmetic} expressions and not as logic
formulas. For this reason, the type notation used in this book denotes
disjunctive types by $A+B$ and tuples by $A\times B$, which is designed
to remind us of arithmetic expressions (such as $1+2$ and $2\times3$)
rather than of logical formulas (such as $A\vee B$ and $A\wedge B$). 

An important use of the type notation is for writing equations with
types. Can we use the arithmetic intuition for writing type equations
such as 
\begin{equation}
\left(A+B\right)\times C=A\times C+B\times C\quad?\label{eq:ch-example-distributive}
\end{equation}
In this section, we will learn how to check whether one type expression
is equivalent to another.

\subsection{Logical identity does not correspond to type equivalence\label{subsec:Logical-identity-not-type-equivalence}}

The CH correspondence maps Eq.~(\ref{eq:ch-example-distributive})
into the logic formula
\begin{equation}
\forall(A,B,C).\,\left(A\vee B\right)\wedge C=\left(A\wedge C\right)\vee\left(B\wedge C\right)\quad.\label{eq:ch-example-distributive-1}
\end{equation}
This formula is the well-known \textsf{``}distributive law\textsf{''}\footnote{\texttt{\href{https://en.wikipedia.org/wiki/Distributive_property\#Rule_of_replacement}{https://en.wikipedia.org/wiki/Distributive\_property\#Rule\_of\_replacement}}}
valid in Boolean logic as well as in the constructive logic. Since
a logical equation $P=Q$ means $P\Rightarrow Q$ and $Q\Rightarrow P$,
the distributive law~(\ref{eq:ch-example-distributive-1}) means
that the two formulas hold,
\begin{align}
 & \forall(A,B,C).\,\left(A\vee B\right)\wedge C\Rightarrow\left(A\wedge C\right)\vee\left(B\wedge C\right)\quad,\label{eq:ch-example-distributive-1a}\\
 & \forall(A,B,C).\,\left(A\wedge C\right)\vee\left(B\wedge C\right)\Rightarrow\left(A\vee B\right)\wedge C\quad.\label{eq:ch-example-distributive-1b}
\end{align}
The CH correspondence maps these logical formulas to fully parametric
functions with types
\begin{lstlisting}
def f1[A, B, C]: ((Either[A, B], C))    => Either[(A, C), (B, C)] = ???
def f2[A, B, C]: Either[(A, C), (B, C)] => (Either[A, B], C)      = ???
\end{lstlisting}
In the type notation, these type signatures are written as
\begin{align*}
 & f_{1}^{A,B,C}:\left(A+B\right)\times C\rightarrow A\times C+B\times C\quad,\\
 & f_{2}^{A,B,C}:A\times C+B\times C\rightarrow\left(A+B\right)\times C\quad.
\end{align*}
Since the two logical formulas (\ref{eq:ch-example-distributive-1a})\textendash (\ref{eq:ch-example-distributive-1b})
are true theorems in constructive logic, we expect to be able to implement
the functions \lstinline!f1! and \lstinline!f2!. It is not straightforward
to guess how to combine the proof rules of Table~\ref{tab:Proof-rules-of-constructive-and-boolean}
to obtain proofs of Eqs.~(\ref{eq:ch-example-distributive-1a})\textendash (\ref{eq:ch-example-distributive-1b}).
So, instead of deriving the implementations of \lstinline!f1! and
\lstinline!f2! from the CH correspondence, we will write the Scala
code directly.

To implement \lstinline!f1!, we need to perform pattern matching
on the argument:
\begin{lstlisting}
def f1[A, B, C]: ((Either[A, B], C)) => Either[(A, C), (B, C)] = {
  case (Left(a), c)   => Left((a, c))  // No other choice here.
  case (Right(b), c)  => Right((b, c)) // No other choice here.
}
\end{lstlisting}
In both cases, we have only one possible expression of the correct
type.

Similarly, the implementation of \lstinline!f2! leaves us no choices:

\begin{wrapfigure}{l}{0.65\columnwidth}%
\vspace{-0.5\baselineskip}
\begin{lstlisting}
def f2[A, B, C]: Either[(A, C), (B, C)] => (Either[A, B], C) = {
  case Left((a, c))   => (Left(a), c)  // No other choice here.
  case Right((b, c))  => (Right(b), c) // No other choice here.
}
\end{lstlisting}
\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent The code of \lstinline!f1! and \lstinline!f2! never discards
any given values; in other words, these functions appear to preserve
information. We can formulate this property rigorously as a requirement
that an arbitrary value \lstinline!x: (Either[A, B], C)! be mapped
by \lstinline!f1! to some value \lstinline!y: Either[(A, C), (B, C)]!
and then mapped by \lstinline!f2! back to \emph{the same} value \lstinline!x!.
Similarly, any value \lstinline!y! of type \lstinline!Either[(A, C), (B, C)]!
should be transformed by \lstinline!f2! and then by \lstinline!f1!
back to the same value \lstinline!y!.

Let us write these conditions as equations,
\[
\forall x^{:(A+B)\times C}.\,f_{2}(f_{1}(x))=x\quad,\quad\quad\forall y^{:A\times C+B\times C}.\,f_{1}\left(f_{2}(y)\right)=y\quad.
\]
If these equations hold, it means that all the information in a value
$x^{:(A+B)\times C}$ is completely preserved inside the value $y\triangleq f_{1}(x)$;
the original value $x$ can be recovered as $x=f_{2}(y)$. Then the
function $f_{1}$ is the \textbf{inverse}\index{inverse function}
of $f_{2}$. Conversely, all the information in a value $y^{:A\times C+B\times C}$
is preserved inside $x\triangleq f_{2}(y)$ and can be recovered by
applying $f_{1}$. Since the values $x^{:(A+B)\times C}$ and $y^{:A\times C+B\times C}$
are arbitrary, it will follow that the \emph{data types} themselves,
$\left(A+B\right)\times C$ and $A\times C+B\times C$, carry equivalent
information. Such types are called equivalent\index{types!equivalent}
or isomorphic\index{types!isomorphic}\index{isomorphic types}.

Generally, we say that types $P$ and $Q$ are \textbf{equivalent}
or \textbf{isomorphic} (denoted $P\cong Q$) \index{type equivalence}when
there exist functions $f_{1}:P\rightarrow Q$ and $f_{2}:Q\rightarrow P$
that are inverses of each other. We can write these conditions using
the notation $(f_{1}\bef f_{2})(x)\triangleq f_{2}(f_{1}(x))$ as
\[
f_{1}\bef f_{2}=\text{id}\quad,\quad\quad f_{2}\bef f_{1}=\text{id}\quad.
\]
(In Scala, the forward composition $f_{1}\bef f_{2}$ is the function
\lstinline!f1 andThen f2!. We omit type annotations since we already
checked that the types match.) If these conditions hold, there is
a one-to-one correspondence between values of types $P$ and $Q$.
This is the same as to say that the data types $P$ and $Q$ \textsf{``}carry
equivalent information\textsf{''}.

To verify that the Scala functions \lstinline!f1! and \lstinline!f2!
defined above are inverses of each other, we first check if $f_{1}\bef f_{2}=\text{id}$.
Applying $f_{1}\bef f_{2}$ means to apply $f_{1}$ and then to apply
$f_{2}$ to the result. Begin by applying $f_{1}$ to an arbitrary
value $x^{:(A+B)\times C}$. A value $x$ of that type can be in only
one of the two disjoint cases: a tuple \lstinline!(Left(a), c)! or
a tuple \lstinline!(Right(b), c)!, for some values \lstinline!a:A!,
\lstinline!b:B!, and \lstinline!c:C!. The Scala code of \lstinline!f1!
maps these tuples to \lstinline!Left((a, c))! and to \lstinline!Right((b, c))!
respectively; we can see this directly from the code of \lstinline!f1!.
We then apply $f_{2}$ to those values, which maps them back to a
tuple \lstinline!(Left(a), c)! or a tuple \lstinline!(Right(b), c)!
respectively, according to the code of \lstinline!f2!. These tuples
are exactly the value $x$ we started with. So, applying $f_{1}\bef f_{2}$
to an arbitrary $x^{:(A+B)\times C}$ does not change the value $x$;
this is the same as to say that $f_{1}\bef f_{2}=\text{id}$.

To check whether $f_{2}\bef f_{1}=\text{id}$, we apply $f_{2}$ to
an arbitrary value $y^{:A\times C+B\times C}$, which must be one
of the two disjoint cases, \lstinline!Left((a, c))! or \lstinline!Right((b, c))!.
The code of \lstinline!f2! maps these two cases into tuples \lstinline!(Left(a), c)!
and \lstinline!(Right(b), c)! respectively. Then we apply \lstinline!f1!
and map these tuples back to \lstinline!Left((a, c))! and \lstinline!Right((b, c))!
respectively. It follows that applying $f_{2}$ and then $f_{1}$
will always recover the initial value $y$. In other words, $f_{2}\bef f_{1}=\text{id}$.

By looking at the code of \lstinline!f1! and \lstinline!f2!, we
can directly observe that these functions are inverses of each other:
the tuple pattern \lstinline!(Left(a), c)! is mapped to \lstinline!Left((a, c))!,
and the pattern \lstinline!(Right(b), c)! to \lstinline!Right((b, c))!,
or vice versa. It is visually clear that no information is lost and
that the original values are restored by function compositions $f_{1}\bef f_{2}$
or $f_{2}\bef f_{1}$.

We find that the logical identity~(\ref{eq:ch-example-distributive-1})
leads to an equivalence of the corresponding types,
\begin{equation}
\left(A+B\right)\times C\cong A\times C+B\times C\quad.\label{eq:ch-distributive-law-types}
\end{equation}
To get Eq.~(\ref{eq:ch-distributive-law-types}) from Eq.~(\ref{eq:ch-example-distributive-1}),
we need convert a logical formula to an arithmetic expression by mentally
replacing the disjunction operations $\vee$ by $+$ and the conjunctions
$\wedge$ by $\times$ everywhere.

Consider another example of a logical identity: the associativity
law for conjunction,
\begin{equation}
\left(\alpha\wedge\beta\right)\wedge\gamma=\alpha\wedge\left(\beta\wedge\gamma\right)\quad.\label{eq:ch-example-associativity-conjunction}
\end{equation}
The corresponding types are $(A\times B)\times C$ and $A\times(B\times C)$;
in Scala, \lstinline!((A, B), C)! and \lstinline!(A, (B, C))!. We
can define functions that convert between these types without information
loss\index{information loss}:
\begin{lstlisting}
def f3[A, B, C]: (((A, B), C)) => (A, (B, C)) = { case ((a, b), c) => (a, (b, c)) }
def f4[A, B, C]: (A, (B, C)) => (((A, B), C)) = { case (a, (b, c)) => ((a, b), c) }
\end{lstlisting}
By applying these functions to arbitrary values of types \lstinline!((A, B), C)!
and \lstinline!(A, (B, C))!, it is easy to see that the functions
\lstinline!f3! and \lstinline!f4! are inverses of each other. This
is also directly visible in the code: the nested tuple pattern \lstinline!((a, b), c)!
is mapped to the pattern \lstinline!(a, (b, c))! and back. So, the
types $\left(A\times B\right)\times C$ and $A\times\left(B\times C\right)$
are equivalent, and we can write $A\times B\times C$ without parentheses.

Does a logical identity always correspond to an equivalence of types?
This turns out to be \emph{not} so. A simple example of a logical
identity that does not correspond to a type equivalence is
\begin{equation}
True\vee\alpha=True\quad.\label{eq:ch-example-logic-identity-2}
\end{equation}
Since the CH correspondence maps the logical constant $True$ into
the unit type $\bbnum 1$, the type equivalence corresponding to Eq.~(\ref{eq:ch-example-logic-identity-2})
is $\bbnum 1+A\cong\bbnum 1$. The type denoted by $\bbnum 1+A$ means
\lstinline!Option[A]! in Scala, so the corresponding equivalence
is \lstinline!Option[A]!$\cong$\lstinline!Unit!. Intuitively, this
type equivalence should not hold: an \lstinline!Option[A]! may carry
a value of type \lstinline!A!, which cannot possibly be stored in
a value of type \lstinline!Unit!. We can verify this intuition rigorously
by proving that any fully parametric functions with type signatures
$g_{1}:\bbnum 1+A\rightarrow\bbnum 1$ and $g_{2}:\bbnum 1\rightarrow\bbnum 1+A$
will not satisfy $g_{1}\bef g_{2}=\text{id}$. To verify this, we
note that $g_{2}:\bbnum 1\rightarrow\bbnum 1+A$ must have type signature

\begin{wrapfigure}{l}{0.4\columnwidth}%
\vspace{-0.8\baselineskip}
\begin{lstlisting}
def g2[A]: Unit => Option[A] = ???
\end{lstlisting}

\vspace{-1\baselineskip}
\end{wrapfigure}%

\noindent Such a function must always return \lstinline!None!, since
a fully parametric function cannot produce values of an arbitrary
type \lstinline!A! from scratch. Therefore, $g_{1}\bef g_{2}$ is
also a function that always returns \lstinline!None!. The function
$g_{1}\bef g_{2}$ has type signature $\bbnum 1+A\rightarrow\bbnum 1+A$
or, in Scala syntax, \lstinline!Option[A] => Option[A]!, and is not
equal to the identity function, because the identity function does
not \emph{always} return \lstinline!None!.

Another example of a logical identity without a type equivalence is
the distributive law 
\begin{equation}
\forall(A,B,C).\,\left(A\wedge B\right)\vee C=\left(A\vee C\right)\wedge\left(B\vee C\right)\quad,\label{eq:ch-example-distributive-2}
\end{equation}
which is \textsf{``}dual\textsf{''} to the law~(\ref{eq:ch-example-distributive-1}),
i.e., it is obtained from Eq.~(\ref{eq:ch-example-distributive-1})
by swapping all conjunctions ($\wedge$) with disjunctions ($\vee$).
In logic, a dual formula to an identity is often also an identity.
The CH correspondence maps Eq.~(\ref{eq:ch-example-distributive-2})
into the type equation
\begin{equation}
\forall(A,B,C).\,\left(A\times B\right)+C=\left(A+C\right)\times\left(B+C\right)\quad.\label{eq:ch-example-incorrect-identity-2}
\end{equation}
However, the types $A\times B+C$ and $\left(A+C\right)\times\left(B+C\right)$
are \emph{not} equivalent. To see why, look at the possible code of
the function $g_{3}:\left(A+C\right)\times\left(B+C\right)\rightarrow A\times B+C$:
\begin{lstlisting}[numbers=left]
def g3[A,B,C]: ((Either[A, C], Either[B, C])) => Either[(A, B), C] = {
  case (Left(a), Left(b))      => Left((a, b)) // No other choice.
  case (Left(a), Right(c))     => Right(c)     // No other choice.
  case (Right(c), Left(b))     => Right(c)     // No other choice.
  case (Right(c1), Right(c2))  => Right(c1)    // Must discard c1 or c2 here!
}   // May return Right(c2) instead of Right(c1) in the last line.
\end{lstlisting}
In line 5, we have a choice of returning \lstinline!Right(c1)! or
\lstinline!Right(c2)!. Whichever we choose, we will lose information\index{information loss}
because we will have discarded one of the given values \lstinline!c1!,
\lstinline!c2!. After evaluating $g_{3}$, we will not be able to
restore \emph{both} \lstinline!c1! and \lstinline!c2!, no matter
what code we write for $g_{4}$. So, the composition $g_{3}\bef g_{4}$
cannot be equal to the identity function. The type equation~(\ref{eq:ch-example-incorrect-identity-2})
is incorrect.

We conclude that a logical identity ${\cal CH}(P)={\cal CH}(Q)$ guarantees,
via the CH correspondence, that we can implement \emph{some} fully
parametric functions of types $P\rightarrow Q$ and $Q\rightarrow P$.
However, it is not guaranteed that these functions are inverses of
each other, i.e., that the type conversions $P\rightarrow Q$ or $Q\rightarrow P$
have no information loss\index{information loss}. So, the type equivalence
$P\cong Q$ does not automatically follow from the logical identity
${\cal CH}(P)={\cal CH}(Q)$.

The CH correspondence means that we can compute \emph{some} value
$x^{:X}$ of a given type $X$ when the proposition ${\cal CH}(X)$
holds. However, the CH correspondence does not guarantee that the
computed value $x^{:X}$ will satisfy any additional properties or
laws.

\subsection{Arithmetic identity corresponds to type equivalence}

Looking at the examples of equivalent types, we notice that correct
type equivalences correspond to \emph{arithmetical} identities rather
than \emph{logical} identities. For instance, the logical identity
in Eq.~(\ref{eq:ch-example-distributive-1}) leads to the type equivalence~(\ref{eq:ch-distributive-law-types}),
which looks like a standard identity of arithmetic, such as
\[
(1+10)\times20=1\times20+10\times20\quad.
\]
The logical identity in Eq.~(\ref{eq:ch-example-distributive-2}),
which does \emph{not} yield a type equivalence, leads to an incorrect
arithmetic equation~\ref{eq:ch-example-incorrect-identity-2}, e.g.,
$\left(1\times10\right)+20\neq\left(1+20\right)\times\left(10+20\right)$.
Similarly, the associativity law~(\ref{eq:ch-example-associativity-conjunction})
leads to a type equivalence and to the arithmetic identity
\[
\left(a\times b\right)\times c=a\times\left(b\times c\right)\quad,
\]
while the logical identity in Eq.~(\ref{eq:ch-example-logic-identity-2}),
which does not yield a type equivalence, leads to an incorrect arithmetic
statement ($\forall a.\,1+a=1$).

Table~\ref{tab:Logical-identities-with-disjunction-and-conjunction}
summarizes these and other examples of logical identities, with the
corresponding type equivalences. In all rows, quantifiers such as
$\forall\alpha$ or $\forall(A,B)$ are implied when necessary.

Because we chose the type notation to be similar to the ordinary arithmetic
notation, it is easy to translate a possible type equivalence into
an arithmetic equation. In all cases, valid arithmetic identities
correspond to type equivalences, and failures to obtain a type equivalence
correspond to incorrect arithmetic identities. With regard to type
equivalence, types such as $A+B$ and $A\times B$ behave similarly
to arithmetic expressions such as $10+20$ and $10\times20$ and not
similarly to logical formulas such as $\alpha\vee\beta$ and $\alpha\wedge\beta$.

\begin{table}
\begin{centering}
\begin{tabular}{|c|c|}
\hline 
\textbf{\small{}Logical identity} & \textbf{\small{}Type equivalence (if it holds)}\tabularnewline
\hline 
\hline 
{\small{}$True\vee\alpha=True$} & {\small{}$\bbnum 1+A\not\cong\bbnum 1$}\tabularnewline
\hline 
{\small{}$True\wedge\alpha=\alpha$} & {\small{}$\bbnum 1\times A\cong A$}\tabularnewline
\hline 
{\small{}$False\vee\alpha=\alpha$} & {\small{}$\bbnum 0+A\cong A$}\tabularnewline
\hline 
{\small{}$False\wedge\alpha=False$} & {\small{}$\bbnum 0\times A\cong\bbnum 0$}\tabularnewline
\hline 
{\small{}$\alpha\vee\beta=\beta\vee\alpha$} & {\small{}$A+B\cong B+A$}\tabularnewline
\hline 
{\small{}$\alpha\wedge\beta=\beta\wedge\alpha$} & {\small{}$A\times B\cong B\times A$}\tabularnewline
\hline 
{\small{}$\left(\alpha\vee\beta\right)\vee\gamma=\alpha\vee\left(\beta\vee\gamma\right)$} & {\small{}$\left(A+B\right)+C\cong A+\left(B+C\right)$}\tabularnewline
\hline 
{\small{}$\left(\alpha\wedge\beta\right)\wedge\gamma=\alpha\wedge\left(\beta\wedge\gamma\right)$} & {\small{}$\left(A\times B\right)\times C\cong A\times\left(B\times C\right)$}\tabularnewline
\hline 
{\small{}$\left(\alpha\vee\beta\right)\wedge\gamma=\left(\alpha\wedge\gamma\right)\vee\left(\beta\wedge\gamma\right)$} & {\small{}$\left(A+B\right)\times C\cong A\times C+B\times C$}\tabularnewline
\hline 
{\small{}$\left(\alpha\wedge\beta\right)\vee\gamma=\left(\alpha\vee\gamma\right)\wedge\left(\beta\vee\gamma\right)$} & {\small{}$\left(A\times B\right)+C\not\cong\left(A+C\right)\times\left(B+C\right)$}\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{Logic identities with disjunction and conjunction, and the corresponding
equivalences of types.\label{tab:Logical-identities-with-disjunction-and-conjunction}}
\end{table}

We already verified the first line and the last three lines of Table~\ref{tab:Logical-identities-with-disjunction-and-conjunction}.
Other identities are verified in a similar way. Let us begin with
lines 3 and 4 of Table~\ref{tab:Logical-identities-with-disjunction-and-conjunction},
which involve the proposition $False$ and the corresponding \index{void type}void
type $\bbnum 0$ (Scala\textsf{'}s \lstinline!Nothing!). Reasoning about the
void type needs a special technique that we will now develop while
verifying the type isomorphisms $\bbnum 0\times A\cong\bbnum 0$ and
$\bbnum 0+A\cong A$.

\subsubsection{Example \label{subsec:ch-Example-0-times-A}\ref{subsec:ch-Example-0-times-A}\index{solved examples}}

Verify the type equivalence $\bbnum 0\times A\cong\bbnum 0$.

\subparagraph{Solution}

Recall that the type notation $\bbnum 0\times A$ represents the Scala
tuple type \lstinline!(Nothing, A)!. To demonstrate that the type
\lstinline!(Nothing, A)! is equivalent to the type \lstinline!Nothing!,
we need to show that the type \lstinline!(Nothing, A)! has \emph{no}
values. Indeed, how could we create a value of type, say, \lstinline!(Nothing, Int)!?
We would need to fill \emph{both} parts of the tuple. We have values
of type \lstinline!Int!, but we can never get a value of type \lstinline!Nothing!.
So, regardless of the type \lstinline!A!, it is impossible to create
any values of type \lstinline!(Nothing, A)!. In other words, the
set of values of the type \lstinline!(Nothing, A)! is empty; but
that is the definition of the void type \lstinline!Nothing!. The
types \lstinline!(Nothing, A)! (denoted by $\bbnum 0\times A$) and
\lstinline!Nothing! (denoted by $\bbnum 0$) are both void and therefore
equivalent.

\subsubsection{Example \label{subsec:ch-Example-0-plus-A}\ref{subsec:ch-Example-0-plus-A}}

Verify the type equivalence $\bbnum 0+A\cong A$.

\subparagraph{Solution}

Recall that the type notation $\bbnum 0+A$ represents the Scala type
\lstinline!Either[Nothing, A]!. We need to show that any value of
that type can be mapped without loss of information to a value of
type \lstinline!A!, and vice versa. This means implementing functions
$f_{1}:\bbnum 0+A\rightarrow A$ and $f_{2}:A\rightarrow\bbnum 0+A$
such that $f_{1}\bef f_{2}=\text{id}$ and $f_{2}\bef f_{1}=\text{id}$.

The argument of $f_{1}$ is of type \lstinline!Either[Nothing, A]!.
How can we create a value of that type? Our only choices are to create
a \lstinline!Left(x)! with \lstinline!x:Nothing!, or to create a
\lstinline!Right(y)! with \lstinline!y:A!. However, we cannot create
a value \lstinline!x! of type \lstinline!Nothing! because the type
\lstinline!Nothing! has \emph{no} values; so we cannot create a \lstinline!Left(x)!.
The only remaining possibility is to create a \lstinline!Right(y)!
with some value \lstinline!y! of type \lstinline!A!. So, any values
of type $\bbnum 0+A$ must be of the form \lstinline!Right(y)!, and
we can extract that \lstinline!y! to obtain a value of type \lstinline!A!:
\begin{lstlisting}
def f1[A]: Either[Nothing, A] => A = {
  case Right(y) => y
  // No need for `case Left(x) => ...` since no `x` can ever be given in `Left(x)`.
}
\end{lstlisting}
For the same reason, there is only one implementation of the function
\lstinline!f2!,
\begin{lstlisting}
def f2[A]: A => Either[Nothing, A] = { y => Right(y) }
\end{lstlisting}
It is clear from the code that the functions \lstinline!f1! and \lstinline!f2!
are inverses of each other.

We have just seen that a value of type $\bbnum 0+A$ is always a \lstinline!Right(y)!
with some \lstinline!y:A!. Similarly, a value of type $A+\bbnum 0$
is always a \lstinline!Left(x)! with some \lstinline!x:A!. So, we
will use the notation $A+\bbnum 0$ and $\bbnum 0+A$ to \emph{denote}
the \lstinline!Left! and the \lstinline!Right! parts of the disjunctive
type \lstinline!Either!. This notation agrees with the behavior of
the Scala compiler, which will infer the types \lstinline!Either[A, Nothing] !or
\lstinline!Either[Nothing, A]! for these parts:

\begin{wrapfigure}{l}{0.53\columnwidth}%
\vspace{-0.5\baselineskip}
\begin{lstlisting}
def toLeft[A, B]: A => Either[A, B] = x => Left(x)
def toRight[A, B]: B => Either[A, B] = y => Right(y)

scala> toLeft(123)
res0: Either[Int, Nothing] = Left(123)

scala> toRight("abc")
res1: Either[Nothing, String] = Right("abc")
\end{lstlisting}

\vspace{-2\baselineskip}
\end{wrapfigure}%

\noindent We can write the functions \lstinline!toLeft! and \lstinline!toRight!
in a code notation as 
\begin{align*}
 & \text{toLeft}^{A,B}=x^{:A}\rightarrow x^{:A}+\bbnum 0^{:B}\quad,\\
 & \text{toRight}^{A,B}=y^{:B}\rightarrow\bbnum 0^{:A}+y^{:B}\quad.
\end{align*}
In this notation, a value of the disjunctive type is shown without
using Scala class names such as \lstinline!Either!, \lstinline!Right!,
and \lstinline!Left!. This shortens the writing and speeds up code
reasoning.

The type annotation $\bbnum 0^{:A}$ is helpful to remind ourselves
about the type parameter $A$ used e.g., by the disjunctive value
$\bbnum 0^{:A}+y^{:B}$ in the body of \lstinline!toRight[A, B]!.
Without this type annotation, $\bbnum 0+y^{:B}$ means a value of
type \lstinline!Either[A, B]! where the parameter $A$ is left unspecified
and should be determined by matching the types of other expressions.

In the notation $\bbnum 0+y^{:B}$, we use the symbol $\bbnum 0$
rather than an ordinary zero ($0$), to avoid suggesting that $0$
is a value of type $\bbnum 0$. The void type $\bbnum 0$ has no values,
unlike the \lstinline!Unit! type, $\bbnum 1$, which has a value
denoted by $1$ in the code notation.

\subsubsection{Example \label{subsec:ch-Example-1xA}\ref{subsec:ch-Example-1xA}}

Verify the type equivalence $A\times\bbnum 1\cong A$.

\subparagraph{Solution}

The corresponding Scala types are the tuple \lstinline!(A, Unit)!
and the type \lstinline!A!. We need to implement functions $f_{1}:\forall A.\,A\times\bbnum 1\rightarrow A$
and $f_{2}:\forall A.\,A\rightarrow A\times\bbnum 1$ and to demonstrate
that they are inverses of each other. The Scala code for these functions
is
\begin{lstlisting}
def f1[A]: ((A, Unit)) => A = { case (a, ()) => a }
def f2[A]: A => (A, Unit) = { a => (a, ()) }
\end{lstlisting}
Let us first write a proof by reasoning directly with Scala code:
\begin{lstlisting}
(f1 andThen f2)((a,())) == f2(f1((a,())) == f2(a) == (a, ())
(f2 andThen f1)(a) == f1(f2(a)) == f1((a, ())) = a
\end{lstlisting}
Now let us write a proof in the code notation. The codes of $f_{1}$
and $f_{2}$ are
\begin{align*}
f_{1} & =a^{:A}\times1\rightarrow a\quad,\\
f_{2} & =a^{:A}\rightarrow a\times1\quad,
\end{align*}
where we denoted by $1$ the value \lstinline!()! of the \lstinline!Unit!
type. We find
\begin{align*}
(f_{1}\bef f_{2})(a^{:A}\times1) & =f_{2}\left(f_{1}(a\times1)\right)=f_{2}\left(a\right)=a\times1\quad,\\
(f_{2}\bef f_{1})(a^{:A}) & =f_{1}(f_{2}(a))=f_{1}(a\times1)=a\quad.
\end{align*}
This shows that both compositions are identity functions. Another
way of writing the proof is by computing the function compositions
symbolically, without applying to a value $a^{:A}$,
\begin{align*}
f_{1}\bef f_{2} & =\left(a\times1\rightarrow a\right)\bef\left(a\rightarrow a\times1\right)=\left(a\times1\rightarrow a\times1\right)=\text{id}^{A\times\bbnum 1}\quad,\\
f_{2}\bef f_{1} & =\left(a\rightarrow a\times1\right)\bef\left(a\times1\rightarrow a\right)=\left(a\rightarrow a\right)=\text{id}^{A}\quad.
\end{align*}


\subsubsection{Example \label{subsec:ch-Example-A+B}\ref{subsec:ch-Example-A+B}}

Verify the type equivalence $A+B\cong B+A$.

\subparagraph{Solution}

The corresponding Scala types are \lstinline!Either[A, B]! and \lstinline!Either[B, A]!.
We use pattern matching to implement the functions required for the
type equivalence:

\begin{wrapfigure}{l}{0.55\columnwidth}%
\vspace{-0.86\baselineskip}
\begin{lstlisting}
def f1[A, B]: Either[A, B] => Either[B, A] = {
  case Left(a)    => Right(a) // No other choice here.
  case Right(b)   => Left(b)  // No other choice here.
}
def f2[A, B]: Either[B, A] => Either[A, B] = f1[B, A]
\end{lstlisting}

\vspace{-1.2\baselineskip}
\end{wrapfigure}%
The functions \lstinline!f1! and \lstinline!f2! are implemented
by code that can be derived unambiguously from the type signatures.
For instance, the line \lstinline!case Left(a) => ...! is required
to return a value of type \lstinline!Either[B, A]! by using only
a given value \lstinline!a:A!. The only way of doing that is by returning
\lstinline!Right(a)!.

It is clear from the code that the functions \lstinline!f1! and \lstinline!f2!
are inverses of each other. To verify that rigorously, we need show
that \lstinline!f1 andThen f2! is equal to an identity function.
The function \lstinline!f1 andThen f2! applies \lstinline!f2! to
the result of \lstinline!f1!. The code of \lstinline!f1! contains
two \lstinline!case ...! lines, each returning a result. So, we need
to apply \lstinline!f2! separately in each line. Evaluate the code
symbolically:
\begin{lstlisting}
(f1 andThen f2) == {
  case Left(a)    => f2(Right(a))
  case Right(b)   => f2(Left(b))
} == {
  case Left(a)    => Left(a)
  case Right(b)   => Right(b)
}
\end{lstlisting}
The result is a function of type \lstinline!Either[A, B] => Either[A, B]!
that does not change its argument; so it is equal to the identity
function. 

Let us now write the function \lstinline!f1! in the code notation
and perform the same derivation. We will also develop a useful notation
for functions operating on disjunctive types.

The pattern matching construction in the Scala code of \lstinline!f1!
contains a pair of functions with types \lstinline!A => Either[B, A]!
and \lstinline!B => Either[B, A]!. One of these functions is chosen
depending on whether the argument of \lstinline!f1! has type $A+\bbnum 0$
or $\bbnum 0+B$. So, we may write the code of \lstinline!f1! as
\[
f_{1}\triangleq x^{:A+B}\rightarrow\begin{cases}
\text{if }x=a^{:A}+\bbnum 0^{:B}\quad: & \bbnum 0^{:B}+a^{:A}\\
\text{if }x=\bbnum 0^{:A}+b^{:B}\quad: & b^{:B}+\bbnum 0^{:A}
\end{cases}
\]
Since both the argument and the result of $f_{1}$ are disjunctive
types with $2$ parts each, it is convenient to write the code of
$f_{1}$ as a $2\times2$ matrix that maps the input parts to the
output parts:\index{disjunctive type!in matrix notation}\index{matrix notation}\begin{wrapfigure}{l}{0.5\columnwidth}%
\vspace{-0.5\baselineskip}
\begin{lstlisting}
def f1[A, B]: Either[A, B] => Either[B, A] = {
  case Left(a)    => Right(a)
  case Right(b)   => Left(b)
}
\end{lstlisting}
\vspace{-2\baselineskip}
\end{wrapfigure}%
\vspace{-0.6\baselineskip}
\[
f_{1}\triangleq\,\begin{array}{|c||cc|}
 & B & A\\
\hline A~ & \bbnum 0 & a^{:A}\rightarrow a\\
B~ & b^{:B}\rightarrow b & \bbnum 0
\end{array}\quad.
\]
\vspace{-0.5\baselineskip}

The rows of the matrix correspond to the \lstinline!case! rows in
the Scala code; there is one row for each part of the disjunctive
type of the argument. The columns of the matrix correspond to the
parts of the disjunctive type of the result.\index{pattern matching!in matrix notation}
The double line marks the input types of the functions.

The code of $f_{2}$ is written similarly; let us rename arguments
for clarity:\hfill{}~\begin{wrapfigure}[4]{l}{0.5\columnwidth}%
\vspace{-0.7\baselineskip}
\begin{lstlisting}
def f2[A, B]: Either[B, A] => Either[A, B] = {
  case Left(y)    => Right(y)
  case Right(x)   => Left(x)
}
\end{lstlisting}
\vspace{-1.5\baselineskip}
\end{wrapfigure}%

\vspace{-1.5\baselineskip}
\[
f_{2}\triangleq\,\begin{array}{|c||cc|}
 & A & B\\
\hline B~ & \bbnum 0 & y^{:B}\rightarrow y\\
A~ & x^{:A}\rightarrow x & \bbnum 0
\end{array}\quad.
\]
\vspace{-0.8\baselineskip}

\noindent The forward composition $f_{1}\bef f_{2}$ is computed by
the standard rules of row-by-column matrix multiplication.\footnote{\texttt{\href{https://en.wikipedia.org/wiki/Matrix_multiplication}{https://en.wikipedia.org/wiki/Matrix\_multiplication}}}
Any terms containing $\bbnum 0$ are omitted, and the remaining functions
are composed:
\begin{align*}
f_{1}\bef f_{2} & =\,\begin{array}{|c||cc|}
 & B & A\\
\hline A~ & \bbnum 0 & a^{:A}\rightarrow a\\
B~ & b^{:B}\rightarrow b & \bbnum 0
\end{array}\,\bef\,\begin{array}{|c||cc|}
 & A & B\\
\hline B~ & \bbnum 0 & y^{:B}\rightarrow y\\
A~ & x^{:A}\rightarrow x & \bbnum 0
\end{array}\\
{\color{greenunder}\text{matrix multiplication}:}\quad & =\,\,\begin{array}{|c||cc|}
 & A & B\\
\hline A~ & (a^{:A}\rightarrow a)\bef(x^{:A}\rightarrow x) & \bbnum 0\\
B~ & \bbnum 0 & (b^{:B}\rightarrow b)\bef(y^{:B}\rightarrow y)
\end{array}\\
{\color{greenunder}\text{function composition}:}\quad & =\,\begin{array}{|c||cc|}
 & A & B\\
\hline A~ & \text{id} & \bbnum 0\\
B~ & \bbnum 0 & \text{id}
\end{array}\,=\text{id}^{:A+B\rightarrow A+B}\quad.
\end{align*}
Several features of the matrix notation are helpful in such calculations.
The parts of the code of $f_{1}$ are automatically composed with
the corresponding parts of the code of $f_{2}$. To check that the
types match in the function composition, we just need to compare the
types in the output row $\,\begin{array}{||cc|}
B & A\end{array}\,$ of $f_{1}$ with the input column $\,\begin{array}{||c|}
B\\
A
\end{array}\,$ of $f_{2}$. Once we verified that all types match, we may omit the
type annotations and write the same derivation more concisely as
\begin{align*}
f_{1}\bef f_{2} & =\,\begin{array}{||cc|}
\bbnum 0 & a^{:A}\rightarrow a\\
b^{:B}\rightarrow b & \bbnum 0
\end{array}\,\bef\,\begin{array}{||cc|}
\bbnum 0 & y^{:B}\rightarrow y\\
x^{:A}\rightarrow x & \bbnum 0
\end{array}\\
{\color{greenunder}\text{matrix multiplication}:}\quad & =\,\,\begin{array}{||cc|}
(a^{:A}\rightarrow a)\bef(x^{:A}\rightarrow x) & \bbnum 0\\
\bbnum 0 & (b^{:B}\rightarrow b)\bef(y^{:B}\rightarrow y)
\end{array}\\
{\color{greenunder}\text{function composition}:}\quad & =\,\begin{array}{||cc|}
\text{id} & \bbnum 0\\
\bbnum 0 & \text{id}
\end{array}\,=\text{id}\quad.
\end{align*}
The identity function is represented by the diagonal matrix $\,\begin{array}{||cc|}
\text{id} & \bbnum 0\\
\bbnum 0 & \text{id}
\end{array}$~.

\subsubsection{Exercise \label{subsec:ch-Exercise-AxB}\ref{subsec:ch-Exercise-AxB}\index{exercises}}

Verify the type equivalence $A\times B\cong B\times A$.

\subsubsection{Exercise \label{subsec:ch-Exercise-A+B+C}\ref{subsec:ch-Exercise-A+B+C}}

Verify the type equivalence $\left(A+B\right)+C\cong A+\left(B+C\right)$.
Since Section~\ref{subsec:Logical-identity-not-type-equivalence}
verified the equivalences $\left(A+B\right)+C\cong A+\left(B+C\right)$
and $\left(A\times B\right)\times C\cong A\times\left(B\times C\right)$,
we may write $A+B+C$ and $A\times B\times C$ without any parentheses.

\subsubsection{Exercise \label{subsec:ch-Exercise-A+B2}\ref{subsec:ch-Exercise-A+B2}}

Verify the type equivalence 
\[
\left(A+B\right)\times\left(A+B\right)=A\times A+\bbnum 2\times A\times B+B\times B\quad,
\]
where $\bbnum 2$ denotes the \lstinline!Boolean! type (defined as
$\bbnum 2\triangleq\bbnum 1+\bbnum 1$).

\subsection{Type cardinalities and type equivalence}

To understand why type equivalences are related to arithmetic identities,
consider the question of how many different values a given type can
have.

Begin by counting the number of distinct values for simple types.
For example, the \lstinline!Unit! type has only one distinct value;
the type \lstinline!Nothing! has zero values; the \lstinline!Boolean!
type has two distinct values, \lstinline!true! and \lstinline!false!;
and the type \lstinline!Int! has $2^{32}$ distinct values.

It is more difficult to count the number of distinct values in a type
such as \lstinline!String!, which is equivalent to a list of unknown
length, \lstinline!List[Char]!. However, each computer\textsf{'}s memory is
limited, so there will exist a maximum length for values of type \lstinline!String!,
and so the total number of possible different strings will be finite
(at least, for any given computer).

For a given type $A$, let us denote by $\left|A\right|$ the number
of distinct values of type $A$. The number $\left|A\right|$ is called
the \index{cardinality}\textbf{cardinality} of type $A$; this is
the same as the number of elements in the set of all values of type
$A$. Since any computer\textsf{'}s memory is finite, and since we may assume
that we are already working with the largest possible computer, then
there will be \emph{finitely} many different values of a given type
$A$ that can exist in the computer. So, we may assume that $\left|A\right|$
is always a finite integer value. This assumption will simplify our
reasoning. We will not actually need to compute the precise number
of, say, all the different possible strings; it is sufficient to know
that the set of all strings is finite, so that we can denote its cardinality
by $|\text{String}|$.

The next step is to consider the cardinality of types such as $A\times B$
and $A+B$. If the types $A$ and $B$ have cardinalities $\left|A\right|$
and $\left|B\right|$, it follows that the set of all distinct pairs
\lstinline!(A, B)! has $\left|A\right|\times\left|B\right|$ elements.
So the cardinality of the type $A\times B$ is equal to the (arithmetic)
product of the cardinalities of $A$ and $B$. The set of all pairs
\[
\left\{ (a,b):a\in A,b\in B\right\} 
\]
is also known as the \index{Cartesian product}\textbf{Cartesian product}
of sets $A$ and $B$, and is denoted by $A\times B$. For this reason,
the tuple type is also called the \index{product type}\textbf{product
type}. Accordingly, the type notation adopts the symbol $\times$
for the product type.

The set of all distinct values of the type $A+B$, i.e., of the Scala
type \lstinline!Either[A, B]!, is a disjoint union of the set of
values of the form \lstinline!Left(a)! and the set of values of the
form \lstinline!Right(b)!. It is clear that the cardinalities of
these sets are equal to $\left|A\right|$ and $\left|B\right|$ respectively.
So the cardinality of the type \lstinline!Either[A, B]! is equal
to $\left|A\right|+\left|B\right|$. For this reason, disjunctive
types such as \lstinline!Either[A, B]! are also called \index{sum type}\textbf{sum
types}, and the type notation adopts the symbol $+$ for these types.

We can write our conclusions as
\begin{align*}
\left|A\times B\right| & =\left|A\right|\times\left|B\right|\quad,\\
\left|A+B\right| & =\left|A\right|+\left|B\right|\quad.
\end{align*}
The type notation, $A\times B$ for pairs and $A+B$ for \lstinline!Either[A, B]!,
translates directly into type cardinalities.

The last step is to notice that two types can be equivalent, $P\cong Q$,
only if their cardinalities are equal, $\left|P\right|=\left|Q\right|$.
When the cardinalities are not equal, $\left|P\right|\neq\left|Q\right|$,
it will be impossible to have a one-to-one correspondence between
the sets of values of type $P$ and values of type $Q$. So it will
be impossible to convert values from type $P$ to type $Q$ and back
without loss of information.

We conclude that types are equivalent when a logical identity \emph{and}
an arithmetic identity hold.

The presence of both identities does not automatically guarantee a
useful type equivalence. The fact that information in one type can
be identically stored in another type does not necessarily mean that
it is helpful to do so in a given application.

For example, the types \lstinline!Option[Option[A]]! and \lstinline!Either[Boolean, A]!
are equivalent because both types contain $2+\left|A\right|$ distinct
values. The short notation for these types is $\bbnum 1+\bbnum 1+A$
and $\bbnum 2+A$ respectively (the type Boolean is denoted by $\bbnum 2$
since it has only two distinct values). 

One could easily write code to convert between these types without
loss of information:
\begin{lstlisting}
def f1[A]: Option[Option[A]] => Either[Boolean, A] = {
  case None           => Left(false) // Or maybe Left(true)?
  case Some(None)     => Left(true)
  case Some(Some(x))  => Right(x)
}

def f2[A]: Either[Boolean, A] => Option[Option[A]] = {
  case Left(false)    => None
  case Left(true)     => Some(None)
  case Right(x)       => Some(Some(x))
}
\end{lstlisting}
A sign of trouble is the presence of an arbitrary choice in this code.
In \lstinline!f1!, we could map \lstinline!None! to \lstinline!Left(false)!
or to \lstinline!Left(true)!, and adjust the rest of the code accordingly;
the type equivalence would still hold. So, formally speaking, these
types \emph{are} equivalent, but there is no \textsf{``}natural\textsf{''} choice
of the conversion functions \lstinline!f1! and \lstinline!f2! that
will work correctly in all applications, because the meaning of these
data types is application-dependent. This type equivalence is \textsf{``}accidental\textsf{''}\index{type equivalence!accidental}.

\subsubsection{Example \label{subsec:ch-Example-cardinality-option-either}\ref{subsec:ch-Example-cardinality-option-either}\index{solved examples}}

Are the types \lstinline!Option[A]! and \lstinline!Either[Unit, A]!
equivalent? Check whether the corresponding logic identity and arithmetic
identity hold.

\paragraph{Solution}

Begin by writing the given types in the type notation: \lstinline!Option[A]!
is written as $\bbnum 1+A$, and \lstinline!Either[Unit, A]! is written
also as $\bbnum 1+A$. The notation already indicates that the types
are equivalent. But let us verify explicitly that the type notation
is not misleading here.

To establish type equivalence, we need to implement two fully parametric
functions
\begin{lstlisting}
def f1[A]: Option[A] => Either[Unit, A] = ???
def f2[A]: Either[Unit, A] => Option[A] = ???
\end{lstlisting}
such that $f_{1}\bef f_{2}=\text{id}$ and $f_{2}\bef f_{1}=\text{id}$.
It is straightforward to implement \lstinline!f1! and \lstinline!f2!:
\begin{lstlisting}
def f1[A]: Option[A] => Either[Unit, A] = {
  case None      => Left(())
  case Some(x)   => Right(x)
}
def f2[A]: Either[Unit, A] => Option[A] = {
  case Left(())   => None
  case Right(x)   => Some(x)
}
\end{lstlisting}
The code clearly shows that \lstinline!f1! and \lstinline!f2! are
inverses of each other; this verifies the type equivalence.

The logic identity is $True\vee A=True\vee A$ and holds trivially.
It remains to check the arithmetic identity, which relates the number
of distinct values of types \lstinline!Option[A]! and \lstinline!Either[Unit, A]!.
Assume that the number of distinct values of type \lstinline!A! is
$\left|A\right|$. Any possible value of type \lstinline!Option[A]!
must be either \lstinline!None! or \lstinline!Some(x)!, where \lstinline!x!
is a value of type \lstinline!A!. So the number of distinct values
of type \lstinline!Option[A]! is $1+\left|A\right|$. All possible
values of type \lstinline!Either[Unit, A]! are of the form \lstinline!Left(())!
or \lstinline!Right(x)!, where \lstinline!x! is a value of type
\lstinline!A!. So the number of distinct values of type \lstinline!Either[Unit, A]!
is $1+\left|A\right|$. We see that the arithmetic identity holds:
the types \lstinline!Option[A]! and \lstinline!Either[Unit, A]!
have equally many distinct values.

This example shows that the type notation is helpful for reasoning
about type equivalences. The solution was found immediately when we
wrote the type notation, $\bbnum 1+A$, for the given types.

\subsection{Type equivalence involving function types}

Until now, we have looked at product types and disjunctive types.
Let us now consider type constructions involving function types.

Consider two types $A$ and $B$, whose cardinalities are known as
$\left|A\right|$ and $\left|B\right|$. What is the cardinality of
the set of all maps between given sets $A$ and $B$? In other words,
how many distinct values does the function type $A\rightarrow B$
have? A function \lstinline!f: A => B! needs to select a value of
type $B$ for each possible value of type $A$. Therefore, the number
of different functions \lstinline!f: A => B! is $\left|B\right|^{\left|A\right|}$.
Here, $\left|B\right|^{\left|A\right|}$ denotes the \textbf{numeric
exponent}\index{exponent}, $\left|B\right|$ to the power $\left|A\right|$.
We use this notation only in this chaper and only when it is clear
that we are computing the cardinality of a function type. Otherwise,
superscripts are used in this book for type parameters and type annotations.

For the types $A=B=\text{Int}$, we have $\left|A\right|=\left|B\right|=2^{32}$,
and so the estimate will give 
\[
\left|A\rightarrow B\right|=(2^{32})^{\left(2^{32}\right)}=2^{32\times2^{32}}=2^{2^{37}}\approx10^{4.1\times10^{10}}\quad.
\]
In fact, most of these functions will map integers to integers in
a complicated (and practically useless) way and will be impossible
to implement on a realistic computer because their code will be much
longer than the available memory. So, the number of practically implementable
functions of type $A\rightarrow B$ is often much smaller than $\left|B\right|^{\left|A\right|}$.
Nevertheless, the estimate $\left|B\right|^{\left|A\right|}$ is useful
since it shows the number of distinct functions that are possible
in principle.

Let us now look for logic identities and arithmetic identities involving
function types. Table~\ref{tab:Logical-identities-with-function-types}
lists the available identities and the corresponding type equivalences.
(In the last column, we defined $a\triangleq\left|A\right|$, $b\triangleq\left|B\right|$,
and $c\triangleq\left|C\right|$ for brevity.) 

It is notable that no logic identity is available for the formula
$\alpha\Rightarrow\left(\beta\vee\gamma\right)$, and correspondingly
no type equivalence is available for the type expression $A\rightarrow B+C$
(although there is an identity for $A\rightarrow B\times C$). The
presence of type expressions of the form $A\rightarrow B+C$ makes
type reasoning more complicated because they cannot be transformed
into equivalent formulas with simpler parts.

\begin{table}
\begin{centering}
\begin{tabular}{|c|c|c|}
\hline 
\textbf{\small{}Logical identity (if holds)} & \textbf{\small{}Type equivalence} & \textbf{\small{}Arithmetic identity}\tabularnewline
\hline 
\hline 
{\small{}$\left(True\Rightarrow\alpha\right)=\alpha$} & {\small{}$\bbnum 1\rightarrow A\cong A$} & {\small{}$a^{1}=a$}\tabularnewline
\hline 
{\small{}$\left(False\Rightarrow\alpha\right)=True$} & {\small{}$\bbnum 0\rightarrow A\cong\bbnum 1$} & {\small{}$a^{0}=1$}\tabularnewline
\hline 
{\small{}$\left(\alpha\Rightarrow True\right)=True$} & {\small{}$A\rightarrow\bbnum 1\cong\bbnum 1$} & {\small{}$1^{a}=1$}\tabularnewline
\hline 
{\small{}$\left(\alpha\Rightarrow False\right)\neq False$} & {\small{}$A\rightarrow\bbnum 0\not\cong\bbnum 0$} & {\small{}$0^{a}\neq0$}\tabularnewline
\hline 
{\small{}$\left(\alpha\vee\beta\right)\Rightarrow\gamma=\left(\alpha\Rightarrow\gamma\right)\wedge\left(\beta\Rightarrow\gamma\right)$} & {\small{}$A+B\rightarrow C\cong\left(A\rightarrow C\right)\times\left(B\rightarrow C\right)$} & {\small{}$c^{a+b}=c^{a}\times c^{b}$}\tabularnewline
\hline 
{\small{}$(\alpha\wedge\beta)\Rightarrow\gamma=\alpha\Rightarrow\left(\beta\Rightarrow\gamma\right)$} & {\small{}$A\times B\rightarrow C\cong A\rightarrow B\rightarrow C$} & {\small{}$c^{a\times b}=(c^{b})^{a}$}\tabularnewline
\hline 
{\small{}$\alpha\Rightarrow\left(\beta\wedge\gamma\right)=\left(\alpha\Rightarrow\beta\right)\wedge\left(\alpha\Rightarrow\gamma\right)$} & {\small{}$A\rightarrow B\times C\cong\left(A\rightarrow B\right)\times\left(A\rightarrow C\right)$} & {\small{}$\left(b\times c\right)^{a}=b^{a}\times c^{a}$}\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{Logical identities with implication, and the corresponding type equivalences
and arithmetic identities.\label{tab:Logical-identities-with-function-types}}
\end{table}

We will now prove some of the type identities in Table~\ref{tab:Logical-identities-with-function-types}.

\subsubsection{Example \label{subsec:ch-Example-type-identity-f}\ref{subsec:ch-Example-type-identity-f}\index{solved examples}}

Verify the type equivalence $\bbnum 1\rightarrow A\cong A$.

\subparagraph{Solution}

Recall that the type notation $\bbnum 1\rightarrow A$ means the Scala
function type \lstinline!Unit => A!. There is only one value of type
\lstinline!Unit!, so the choice of a function of the type \lstinline!Unit => A!
is the same as the choice of a value of type \lstinline!A!. Thus,
the type $\bbnum 1\rightarrow A$ has$\left|A\right|$ distinct values,
so the arithmetic identity holds.

To verify the type equivalence explicitly, we need to implement two
functions
\begin{lstlisting}
def f1[A]: (Unit => A) => A = ???
def f2[A]: A => Unit => A = ???
\end{lstlisting}
The first function needs to produce a value of type \lstinline!A!,
given an argument of the function type \lstinline!Unit => A!. The
only possibility is to apply that function to the value of type \lstinline!Unit!;
we can always produce that value as \lstinline!()!:
\begin{lstlisting}
def f1[A]: (Unit => A) => A = (h: Unit => A) => h(())
\end{lstlisting}
Implementing \lstinline!f2! is straightforward; we can just discard
the \lstinline!Unit! argument:
\begin{lstlisting}
def f2[A]: A => Unit => A = (x: A) => _ => x
\end{lstlisting}
It remains to show that the functions \lstinline!f1! and \lstinline!f2!
are inverses of each other. Let us perform the proof using Scala code
and then using the code notation.

Writing Scala code, compute \lstinline!f1(f2(x))! for an arbitrary
\lstinline!x:A!. Substituting the code, we get
\begin{lstlisting}
f1(f2(x)) == f1(_ => x) == (_ => x)(()) == x
\end{lstlisting}
Now compute \lstinline!f2(f1(h))! for arbitrary \lstinline!h: Unit => A!
in Scala code:
\begin{lstlisting}
f2(f1(h)) == f2(h(())) == { _ => h(()) }
\end{lstlisting}
How can we show that the function \lstinline!{_ => h(())}! is equal
to \lstinline!h!? Whenever we apply equal functions to equal arguments,
they return equal results. In our case, the argument of \lstinline!h!
is of type \lstinline!Unit!, so we only need to verify that the result
of applying \lstinline!h! to the value \lstinline!()! is the same
as the result of applying \lstinline!{_ => h(())}! to \lstinline!()!.
In other words, we need to apply both sides to an additional argument
\lstinline!()!:
\begin{lstlisting}
f2(f1(h))(()) == { _ => h(()) } (()) == h(())
\end{lstlisting}
This completes the proof.

For comparison, let us show the same proof in the code notation. The
functions $f_{1}$ and $f_{2}$ are 
\begin{align*}
 & f_{1}\triangleq h^{:\bbnum 1\rightarrow A}\rightarrow h(1)\quad,\\
 & f_{2}\triangleq x^{:A}\rightarrow1\rightarrow x\quad.
\end{align*}
Now write the function compositions in both directions:
\begin{align*}
{\color{greenunder}\text{expect to equal }\text{id}:}\quad & f_{1}\bef f_{2}=(h^{:\bbnum 1\rightarrow A}\rightarrow h(1))\bef(x^{:A}\rightarrow1\rightarrow x)\\
{\color{greenunder}\text{compute composition}:}\quad & \quad=h^{:\bbnum 1\rightarrow A}\rightarrow1\rightarrow h(1)\\
{\color{greenunder}\text{note that }1\rightarrow h(1)\text{ is the same as }h:}\quad & \quad=(h^{:\bbnum 1\rightarrow A}\rightarrow h)=\text{id}\quad.\\
{\color{greenunder}\text{expect to equal }\text{id}:}\quad & f_{2}\bef f_{1}=(x^{:A}\rightarrow1\rightarrow x)\bef(h^{:\bbnum 1\rightarrow A}\rightarrow h(1))\\
{\color{greenunder}\text{compute composition}:}\quad & \quad=x^{:A}\rightarrow(1\rightarrow x)(1)\\
{\color{greenunder}\text{apply function}:}\quad & \quad=(x^{:A}\rightarrow x)=\text{id}\quad.
\end{align*}

The type $\bbnum 1\rightarrow A$ is equivalent to the type $A$,
but these types are not the same. The most important difference between
these types is that a value of type $A$ is available immediately,
while a value of type $\bbnum 1\rightarrow A$ is a function that
still needs to be applied to an argument (of type $\bbnum 1$) before
a value of type $A$ is obtained. The type $\bbnum 1\rightarrow A$
may represent an \textsf{``}on-call\textsf{''}\index{on-call value} value of type
$A$; that is, a value computed on demand every time. (See Section~\ref{subsec:Lazy-values-iterators-and-streams}
for more details about \textsf{``}on-call\textsf{''} values.)

The void type\index{void type} $\bbnum 0$ needs special reasoning,
as the next examples show:

\subsubsection{Example \label{subsec:ch-Example-type-identity-0-to-A}\ref{subsec:ch-Example-type-identity-0-to-A}}

Verify the type equivalence $\bbnum 0\rightarrow A\cong\bbnum 1$.

\subparagraph{Solution}

What could be a function $f^{:\bbnum 0\rightarrow A}$ from the type
$\bbnum 0$ to a type $A$? Since there exist no values of type $\bbnum 0$,
the function $f$ will never be applied to any arguments and so \emph{does
not need} to compute any actual values of type $A$. So, $f$ is a
function whose body is \textsf{``}empty\textsf{''}; or at least it does not need to
contain any expressions of type $A$. In Scala, such a function can
be written as
\begin{lstlisting}
def absurd[A]: Nothing => A = { ??? }
\end{lstlisting}
This code will compile without type errors. An equivalent code is
\begin{lstlisting}
def absurd[A]: Nothing => A = { x => ??? }
\end{lstlisting}
The symbol \lstinline!???! is defined in the Scala library and represents
code that is \textsf{``}not implemented\textsf{''}. Trying to evaluate this symbol
will produce an error:
\begin{lstlisting}
scala> ???
scala.NotImplementedError: an implementation is missing
  scala.Predef$.$qmark$qmark$qmark(Predef.scala:288) 
\end{lstlisting}
Since the function \lstinline!absurd! can never be applied to an
argument, this error will never happen. So, we can pretend that the
result value (which will never be computed) has any required type,
e.g., type $A$.

Let us now verify that there exists \emph{only one} distinct function
of type $\bbnum 0\rightarrow A$. Take any two functions of that type,
$f^{:\bbnum 0\rightarrow A}$ and $g^{:\bbnum 0\rightarrow A}$. Are
they different? The only way of showing that $f$ and $g$ are different
is by producing a value $x^{:\bbnum 0}$ such that $f(x)\neq g(x)$.
But there are \emph{no} \emph{values} of type $\bbnum 0$, and for
this reason, we will never be able to find the required value $x^{:\bbnum 0}$.
It follows that any two functions $f$ and $g$ of type $\bbnum 0\rightarrow A$
are equal, $f=g$. In other words, there exists only one distinct
value of type $\bbnum 0\rightarrow A$; i.e., the cardinality of the
type $\bbnum 0\rightarrow A$ is $1$. So, the type $\bbnum 0\rightarrow A$
is equivalent to the type $\bbnum 1$.

\subsubsection{Example \label{subsec:ch-Example-type-identity-A-0}\ref{subsec:ch-Example-type-identity-A-0}}

Show that $A\rightarrow\bbnum 0\not\cong\bbnum 0$ and $A\rightarrow\bbnum 0\not\cong\bbnum 1$.

\subparagraph{Solution}

To prove that two types are \emph{not} equivalent, it is sufficient
to show that their type cardinalities are different. Let us determine
the cardinality of the type $A\rightarrow\bbnum 0$, assuming that
the cardinality of $A$ is known. We note that a function of type,
say, $\text{Int}\rightarrow\bbnum 0$ is impossible to implement.
(If we had such a function $f^{:\text{Int}\rightarrow\bbnum 0}$,
we could evaluate, say, $x\triangleq f(123)$ and obtain a value $x$
of type $\bbnum 0$, which is impossible by definition of the type
$\bbnum 0$. It follows that $\left|\text{Int}\rightarrow\bbnum 0\right|=0$.
However, Example~\ref{subsec:ch-Example-type-identity-0-to-A} shows
that $\bbnum 0\rightarrow\bbnum 0$ has cardinality $1$. So, the
cardinality $\left|A\rightarrow\bbnum 0\right|=1$ if the type $A$
is itself $\bbnum 0$ but $\left|A\rightarrow\bbnum 0\right|=0$ for
all other types $A$. We conclude that the type $A\rightarrow\bbnum 0$
is not equivalent to $\bbnum 0$ or $\bbnum 1$ for all $A$. The
type $A\rightarrow\bbnum 0$ it is equivalent to $\bbnum 0$ only
for non-void types $A$.

\subsubsection{Example \label{subsec:ch-Example-type-identity-2}\ref{subsec:ch-Example-type-identity-2}}

Verify the type equivalence $A\rightarrow\bbnum 1\cong\bbnum 1$.

\subparagraph{Solution}

There is only one fully parametric function that returns $\bbnum 1$:
\begin{lstlisting}
def f[A]: A => Unit = { _ => () }
\end{lstlisting}
The function $f$ cannot use its argument of type $A$ since nothing
is known about that type. So the code of $f$ \emph{must} discard
its argument and return the fixed value \lstinline!()! of type \lstinline!Unit!.
In the code notation, this function is written as
\[
f^{:A\rightarrow\bbnum 1}\triangleq\left(\_\rightarrow1\right)\quad.
\]
We can show that there exist only \emph{one} distinct function of
type $A\rightarrow\bbnum 1$ (that is, the type $A\rightarrow\bbnum 1$
has cardinality $1$). Assume that $f$ and $g$ are two such functions,
and try to find a value $x^{:A}$ such that $f(x)\neq g(x)$. We cannot
find any such $x$ because $f(x)=1$ and $g(x)=1$ for all $x$. So,
any two functions $f$ and $g$ of type $A\rightarrow\bbnum 1$ must
be equal to each other. The cardinality of the type $A\rightarrow\bbnum 1$
is $1$.

Any type having cardinality $1$ is equivalent to the \lstinline!Unit!
type, $\bbnum 1$. So $A\rightarrow\bbnum 1\cong\bbnum 1$.

\subsubsection{Example \label{subsec:ch-Example-type-identity-5}\ref{subsec:ch-Example-type-identity-5}}

Verify the type equivalence 
\[
A+B\rightarrow C\cong(A\rightarrow C)\times(B\rightarrow C)\quad.
\]


\subparagraph{Solution}

Begin by implementing two functions with type signatures
\begin{lstlisting}
def f1[A,B,C]: (Either[A, B] => C) => (A => C, B => C) = ???
def f2[A,B,C]: ((A => C, B => C)) => Either[A, B] => C = ???
\end{lstlisting}
The code can be derived unambiguously from the type signatures. For
the first function, we need to produce a pair of functions of type
\lstinline!(A => C, B => C)!. Can we produce the first part of that
pair? Computing a function of type \lstinline!A => C! means that
we need to produce a value of type \lstinline!C! given an arbitrary
value \lstinline!a:A!. The available data is a function of type \lstinline!Either[A, B] => C!
called, say, \lstinline!h!. We can apply that function to \lstinline!Left(a)!
and obtain a value of type \lstinline!C! as required. So, a function
of type \lstinline!A => C! is computed as \lstinline!a => h(Left(a))!.
Similarly, we produce a function of type \lstinline!B => C!. The
code is
\begin{lstlisting}
def f1[A,B,C]: (Either[A, B] => C) => (A => C, B => C) =
  (h: Either[A, B] => C) => (a => h(Left(a)), b => h(Right(b)))
\end{lstlisting}
A code notation for this function is
\begin{align*}
 & f_{1}:\left(A+B\rightarrow C\right)\rightarrow\left(A\rightarrow C\right)\times\left(B\rightarrow C\right)\quad,\\
 & f_{1}\triangleq h^{:A+B\rightarrow C}\rightarrow\big(a^{:A}\rightarrow h(a+\bbnum 0^{:B})\big)\times\big(b^{:B}\rightarrow h(\bbnum 0^{:A}+b)\big)\quad.
\end{align*}

For the function \lstinline!f2!, we need to apply pattern matching
to both curried arguments and then return a value of type \lstinline!C!.
This can be achieved in only one way:
\begin{lstlisting}
def f2[A,B,C]: ((A => C, B => C)) => Either[A, B] => C = { case (f, g) =>
  {
    case Left(a)    => f(a)
    case Right(b)   => g(b)
  }
}
\end{lstlisting}
A code notation for this function can be written as
\begin{align*}
 & f_{2}:\left(A\rightarrow C\right)\times\left(B\rightarrow C\right)\rightarrow A+B\rightarrow C\quad,\\
 & f_{2}\triangleq f^{:A\rightarrow C}\times g^{:B\rightarrow C}\rightarrow\,\begin{array}{|c||c|}
 & C\\
\hline A & a\rightarrow f(a)\\
B & b\rightarrow g(b)
\end{array}\quad.
\end{align*}
The matrix in the last line has only one column because the result
type, $C$, is not known to be a disjunctive type. We may simplify
the functions, e.g., $a\rightarrow f(a)$ into $f$, and write
\[
f_{2}\triangleq f^{:A\rightarrow C}\times g^{:B\rightarrow C}\rightarrow\,\begin{array}{|c||c|}
 & C\\
\hline A & f\\
B & g
\end{array}\quad.
\]

It remains to verify that $f_{1}\bef f_{2}=\text{id}$ and $f_{2}\bef f_{1}=\text{id}$.
To compute $f_{1}\bef f_{2}$, we write (omitting types)
\begin{align*}
f_{1}\bef f_{2} & =\big(h\rightarrow(a\rightarrow h(a+\bbnum 0))\times(b\rightarrow h(\bbnum 0+b))\big)\bef\bigg(f\times g\rightarrow\,\begin{array}{||c|}
f\\
g
\end{array}\,\bigg)\\
{\color{greenunder}\text{compute composition}:}\quad & =h\rightarrow\,\begin{array}{||c|}
a\rightarrow h(a+\bbnum 0)\\
b\rightarrow h(\bbnum 0+b)
\end{array}\quad.
\end{align*}
To proceed, we need to simplify the expressions $h(a+\bbnum 0)$ and
$h(\bbnum 0+b)$. We rewrite the argument $h$ (an arbitrary function
of type $A+B\rightarrow C$) in the matrix notation:
\[
h\triangleq\,\begin{array}{|c||c|}
 & C\\
\hline A & a\rightarrow p(a)\\
B & b\rightarrow q(b)
\end{array}\,=\,\begin{array}{|c||c|}
 & C\\
\hline A & p\\
B & q
\end{array}\quad,
\]
where $p^{:A\rightarrow C}$ and $q^{:B\rightarrow C}$ are new arbitrary
functions. Since we already checked the types, we can omit all type
annotations and write $h$ as
\[
h\triangleq\,\begin{array}{||c|}
p\\
q
\end{array}\quad.
\]
To evaluate expressions such as $h(a+\bbnum 0)$ and $h(\bbnum 0+b)$,
we need to use one of the rows of the column matrix $h$. The correct
row will be selected \emph{automatically} by the rules of matrix multiplication
if we place a row vector to the left of the matrix and use the convention
of omitting terms containing $\bbnum 0$:
\[
\begin{array}{|cc|}
a & \bbnum 0\end{array}\,\triangleright\,\begin{array}{||c|}
p\\
q
\end{array}\,=a\triangleright p\quad,\quad\quad\begin{array}{|cc|}
\bbnum 0 & b\end{array}\,\triangleright\,\begin{array}{||c|}
p\\
q
\end{array}\,=b\triangleright q\quad.
\]
Here we used the symbol $\triangleright$ to separate an argument
from a function when the argument is written to the \emph{left} of
the function. The symbol $\triangleright$ (pronounced \textsf{``}pipe\textsf{''})
is defined by $x\triangleright f\triangleq f(x)$. In Scala, this
operation is available as \lstinline!x.pipe(f)! as of Scala 2.13.

We can write values of disjunctive types, such as $a+\bbnum 0$, as
row vectors $\,\begin{array}{|cc|}
a & \bbnum 0\end{array}\,$:
\begin{equation}
h(a+\bbnum 0)=(a+\bbnum 0)\triangleright h=\,\begin{array}{|cc|}
a & \bbnum 0\end{array}\,\triangleright\,h\quad.\label{eq:forward-notation-}
\end{equation}
With these notations, we can compute further, by omitting terms containing
$\bbnum 0$:
\begin{align*}
 & h(a+\bbnum 0)=\,\begin{array}{|cc|}
a & \bbnum 0\end{array}\,\triangleright\,\begin{array}{||c|}
p\\
q
\end{array}\,=a\triangleright p=p(a)\quad,\\
 & h(\bbnum 0+b)=\,\,\begin{array}{|cc|}
\bbnum 0 & b\end{array}\,\triangleright\,\begin{array}{||c|}
p\\
q
\end{array}\,=b\triangleright q=q(b)\quad.
\end{align*}
Now we can complete the proof of $f_{1}\bef f_{2}=\text{id}$:
\begin{align*}
f_{1}\bef f_{2} & =h\rightarrow\,\begin{array}{||c|}
a\rightarrow h(a+\bbnum 0)\\
b\rightarrow h(\bbnum 0+b)
\end{array}\\
{\color{greenunder}\text{previous equations}:}\quad & =\,\begin{array}{||c|}
p\\
q
\end{array}\,\rightarrow\,\begin{array}{||c|}
a\rightarrow p(a)\\
b\rightarrow q(b)
\end{array}\\
{\color{greenunder}\text{simplify functions}:}\quad & =\,\,\begin{array}{||c|}
p\\
q
\end{array}\,\rightarrow\,\begin{array}{||c|}
p\\
q
\end{array}\,=\text{id}\quad.
\end{align*}

To prove that $f_{2}\bef f_{1}=\text{id}$, use the notation~(\ref{eq:forward-notation-}):
\begin{align*}
 & f_{2}\bef f_{1}=\bigg(f\times g\rightarrow\,\begin{array}{||c|}
f\\
g
\end{array}\,\bigg)\bef\big(h\rightarrow(a\rightarrow(a+\bbnum 0)\triangleright h)\times(b\rightarrow(\bbnum 0+b)\triangleright h)\big)\\
{\color{greenunder}\text{compute composition}:}\quad & =f\times g\rightarrow\big(a\rightarrow\,\begin{array}{|cc|}
a & \bbnum 0\end{array}\,\triangleright\,\begin{array}{||c|}
f\\
g
\end{array}\,\big)\times\big(b\rightarrow\,\begin{array}{|cc|}
\bbnum 0 & b\end{array}\,\triangleright\,\begin{array}{||c|}
f\\
g
\end{array}\,\big)
\end{align*}
\begin{align*}
{\color{greenunder}\text{matrix notation}:}\quad & =f\times g\rightarrow(a\rightarrow\gunderline{a\triangleright f})\times(b\rightarrow\gunderline{b\triangleright g})\\
{\color{greenunder}\text{definition of }\triangleright:}\quad & =f\times g\rightarrow\gunderline{\left(a\rightarrow f(a)\right)}\times\gunderline{\left(b\rightarrow g(b)\right)}\\
{\color{greenunder}\text{simplify functions}:}\quad & =\left(f\times g\rightarrow f\times g\right)=\text{id}\quad.
\end{align*}

In this way, we have proved that $f_{1}$ and $f_{2}$ are mutual
inverses. The proofs appear long because we took time to motivate
and introduce new notation for applying matrices to row vectors. Given
this notation, the proof for $f_{1}\bef f_{2}=\text{id}$ can be written
as
\begin{align*}
f_{1}\bef f_{2} & =\left(h\rightarrow(a\rightarrow(a+\bbnum 0)\triangleright h)\times(b\rightarrow(\bbnum 0+b)\triangleright h)\right)\bef\bigg(f\times g\rightarrow\,\begin{array}{||c|}
f\\
g
\end{array}\bigg)\\
{\color{greenunder}\text{compute composition}:}\quad & =h\rightarrow\,\begin{array}{||c|}
\,a\,\rightarrow\,\left|\begin{array}{cc}
a & \bbnum 0\end{array}\right|\triangleright h\\
b\rightarrow\left|\begin{array}{cc}
\bbnum 0 & b\end{array}\right|\triangleright h
\end{array}\,=\,\begin{array}{||c|}
p\\
q
\end{array}\rightarrow\,\begin{array}{||c|}
a\rightarrow\,\begin{array}{|cc|}
a & \bbnum 0\end{array}\,\triangleright\,\begin{array}{||c|}
p\\
q
\end{array}\\
b\,\rightarrow\,\begin{array}{|cc|}
\bbnum 0 & b\,\,\end{array}\,\triangleright\,\begin{array}{||c|}
p\\
q
\end{array}
\end{array}\\
{\color{greenunder}\text{matrix notation}:}\quad & =\,\begin{array}{||c|}
p\\
q
\end{array}\,\rightarrow\,\begin{array}{||c|}
a\rightarrow a\triangleright p\\
b\rightarrow b\triangleright q
\end{array}\,=\,\begin{array}{||c|}
p\\
q
\end{array}\,\rightarrow\,\begin{array}{||c|}
p\\
q
\end{array}\,=\text{id}\quad.
\end{align*}
Proofs in the code notation are shorter than in Scala syntax because
many names and keywords (such as \lstinline!Left!, \lstinline!Right!,
\lstinline!case!, \lstinline!match!, etc.) are omitted. From now
on, we will prefer to use the code notation in proofs, keeping in
mind that one can always convert the code notation to Scala and back.

Note that the function arrow ($\rightarrow$) binds weaker than the
pipe operation ($\triangleright$), so the code notation $x\rightarrow y\triangleright z$
means $x\rightarrow(y\triangleright z)$. We will review the code
notation more thoroughly in Chapter~\ref{chap:Reasoning-about-code}.

\subsubsection{Example \label{subsec:ch-Example-type-identity-6}\ref{subsec:ch-Example-type-identity-6}}

Verify the type equivalence 
\[
A\times B\rightarrow C\cong A\rightarrow B\rightarrow C\quad.
\]


\subparagraph{Solution}

Begin by implementing the two functions
\begin{lstlisting}
def f1[A,B,C]: (((A, B)) => C) => A => B => C = ???
def f2[A,B,C]: (A => B => C) => ((A, B)) => C = ???
\end{lstlisting}
The Scala code can be derived from the type signatures unambiguously:
\begin{lstlisting}
def f1[A,B,C]: (((A, B)) => C) => A => B => C = g => a => b => g((a, b))
def f2[A,B,C]: (A => B => C) => ((A, B)) => C = h => { case (a, b) => h(a)(b) }
\end{lstlisting}
Write these functions in the code notation:
\begin{align*}
 & f_{1}=g^{:A\times B\rightarrow C}\rightarrow a^{:A}\rightarrow b^{:B}\rightarrow g(a\times b)\quad,\\
 & f_{2}=h^{:A\rightarrow B\rightarrow C}\rightarrow\left(a\times b\right)^{:A\times B}\rightarrow h(a)(b)\quad.
\end{align*}
We denote by $\left(a\times b\right)^{:A\times B}$ the argument of
type \lstinline!(A, B)! with pattern matching implied. This notation
allows us to write shorter code formulas involving tupled arguments.

Compute the function composition $f_{1}\bef f_{2}$:
\begin{align*}
f_{1}\bef f_{2} & =(g\rightarrow\gunderline{a\rightarrow b\rightarrow g(a\times b)})\bef\left(h\rightarrow a\times b\rightarrow h(a)(b)\right)\\
{\color{greenunder}\text{substitute }h=a\rightarrow b\rightarrow g(a\times b):}\quad & =g\rightarrow\gunderline{a\times b\rightarrow g(a\times b)}\\
{\color{greenunder}\text{simplify function}:}\quad & =\left(g\rightarrow g\right)=\text{id}\quad.
\end{align*}
Compute the function composition $f_{2}\bef f_{1}$:
\begin{align*}
f_{2}\bef f_{1} & =(h\rightarrow\gunderline{a\times b\rightarrow h(a)(b)})\bef\left(g\rightarrow a\rightarrow b\rightarrow g(a\times b)\right)\\
{\color{greenunder}\text{substitute }g=a\times b\rightarrow h(a)(b):}\quad & =h\rightarrow a\rightarrow\gunderline{b\rightarrow h(a)(b)}\\
{\color{greenunder}\text{simplify function }b\rightarrow h(a)(b):}\quad & =h\rightarrow\gunderline{a\rightarrow h(a)}\\
{\color{greenunder}\text{simplify function }a\rightarrow h(a)\text{ to }h:}\quad & =\left(h\rightarrow h\right)=\text{id}\quad.
\end{align*}


\subsubsection{Exercise \label{subsec:ch-solvedExample-5-1}\ref{subsec:ch-solvedExample-5-1}\index{exercises}}

Verify the type equivalence $\left(A\rightarrow B\times C\right)\cong\left(A\rightarrow B\right)\times\left(A\rightarrow C\right)\quad.$

\section{Summary}

What tasks can we perform now?
\begin{itemize}
\item Convert a fully parametric type signature into a logical formula to:
\begin{itemize}
\item Decide whether the type signature can be implemented in code.
\item If possible, derive the code using the CH correspondence.
\end{itemize}
\item Use the type notation (Table~\ref{tab:ch-correspondence-type-notation-CH-propositions})
for reasoning about types to:
\begin{itemize}
\item Decide type equivalence using the rules in Tables~\ref{tab:Logical-identities-with-disjunction-and-conjunction}\textendash \ref{tab:Logical-identities-with-function-types}.
\item Simplify type expressions before writing code.
\end{itemize}
\item Use the matrix notation and the pipe notation to write code that works
on disjunctive types.
\end{itemize}
What tasks \emph{cannot} be performed with these tools?
\begin{itemize}
\item Automatically generate code for a \emph{recursive} function. (The
CH correspondence is based on propositional logic, which cannot describe
recursion. Accordingly, recursion is absent from the eight code constructions
of Section~\ref{subsec:The-rules-of-proof}.)
\item Automatically generate code satisfying a property (e.g., isomorphism).
We may generate the code, but it is not guaranteed that properties
will hold. The workaround is to verify the required properties manually,
after deriving the code.
\item Express complicated conditions (e.g., \textsf{``}array is sorted\textsf{''}) in a
type signature. This can be done using \textbf{dependent types}\index{dependent type}
(i.e., types that depend on run-time values in an arbitrary way) \textemdash{}
an advanced technique for which Scala has limited support. (Programming
languages such as Coq, Agda, and Idris support full dependent types.)
\item Generate code using type constructors with known properties (e.g.,\ the
\lstinline!map! method).
\end{itemize}
As an example of using type constructors with properties, consider
this type signature:
\begin{lstlisting}
def q[A]: Array[A] => (A => Option[B]) => Array[Option[B]]
\end{lstlisting}
Can we generate the code of this function from its type signature?
We know that the Scala library defines a \lstinline!map! method on
the \lstinline!Array! type constructor, so the implementation of
\lstinline!q! is simple,
\begin{lstlisting}
def q[A]: Array[A] => (A => Option[B]) => Array[Option[B]] = { arr => f => arr.map(f) }
\end{lstlisting}
However, it is hard to create an \emph{algorithm} that can derive
this implementation automatically from the type signature of \lstinline!q!
via the Curry-Howard correspondence. The algorithm would have to convert
the type signature of \lstinline!q! into the logical formula 
\begin{equation}
{\cal CH}(\text{Array}^{A})\Rightarrow{\cal CH}(A\rightarrow\text{Opt}^{B})\Rightarrow{\cal CH}(\text{Array}^{\text{Opt}^{B}})\quad.\label{eq:ch-example-quantified-proposition}
\end{equation}
To derive an implementation, the algorithm would need to use the available
\lstinline!map! method for \lstinline!Array!. That method has the
type signature
\[
\text{map}:\forall(A,B).\,\text{Array}^{A}\rightarrow\left(A\rightarrow B\right)\rightarrow\text{Array}^{B}\quad.
\]
To derive the ${\cal CH}$-proposition~(\ref{eq:ch-example-quantified-proposition}),
the algorithm will need to assume that the ${\cal CH}$-proposition
\begin{equation}
{\cal CH}\,\big(\forall(A,B).\,\text{Array}^{A}\rightarrow\left(A\rightarrow B\right)\rightarrow\text{Array}^{B}\big)\label{eq:ch-example-quantified-proposition-2}
\end{equation}
already holds, i.e., that Eq.~(\ref{eq:ch-example-quantified-proposition-2})
is one of the premises of a sequent to be proved. Reasoning about
propositions such as Eq.~(\ref{eq:ch-example-quantified-proposition-2})
requires \index{first-order logic}\textbf{first-order logic} \textemdash{}
a logic whose proof rules can handle quantified types such as $\forall(A,B)$\emph{
inside} premises. However, first-order logic is \textbf{undecidable}\index{undecidable logic}:
no algorithm can guarantee finding a proof or showing the absence
of a proof in all cases. 

The constructive propositional logic (with the rules listed in Section~\ref{subsec:The-rules-of-proof})
is \textbf{decidable},\index{decidable logic} i.e., it has an algorithm
that either finds a proof or disproves any given formula. However,
that logic cannot handle type constructors such as $\text{Array}^{A}$.
It also cannot handle premises with type quantifiers such as $\forall(A,B)$
inside, because all the available rules have the quantifiers placed
\emph{outside} the premises. 

So, code for functions such as \lstinline!q! can only be derived
by trial and error, informed by intuition. This book will help programmers
to acquire the necessary intuition and technique.

\subsection{Solved examples\index{solved examples}}

\subsubsection{Example \label{subsec:ch-solvedExample-1}\ref{subsec:ch-solvedExample-1}}

Find the cardinality of the type \lstinline!P = Option[Option[Boolean] => Boolean]!.
Write \lstinline!P! in the type notation and simplify to an equivalent
type.

\subparagraph{Solution}

Begin with the type \lstinline!Option[Boolean]!, which can be either
\lstinline!None! or \lstinline!Some(x)! with an \lstinline!x:Boolean!.
Since the type \lstinline!Boolean! has $2$ possible values, the
type \lstinline!Option[Boolean]! has $3$ values:
\[
|\text{Opt}^{\text{Boolean}}|=\left|\bbnum 1+\text{Boolean}\right|=1+\left|\text{Boolean}\right|=3\quad.
\]
In the type notation, \lstinline!Boolean! is denoted by the symbol
$\bbnum 2$, and the type \lstinline!Option[Boolean]! by $\bbnum 1+\bbnum 2$.
So, the type notation $\bbnum 1+\bbnum 2$ is consistent with the
cardinality $3$ of that type,
\[
\left|\bbnum 1+\text{Boolean}\right|=\left|\bbnum 1+\bbnum 2\right|=1+2=3\quad.
\]

The function type \lstinline!Option[Boolean] => Boolean! is denoted
by $\bbnum 1+\bbnum 2\rightarrow\bbnum 2$. Its cardinality is computed
as the arithmetic power 
\[
|\text{Opt}^{\text{Boolean}}\rightarrow\text{Boolean}|=\left|\bbnum 1+\bbnum 2\rightarrow\bbnum 2\right|=\left|\bbnum 2\right|^{\left|\bbnum 1+\bbnum 2\right|}=2^{3}=8\quad.
\]
Finally, the we write \lstinline!P! in the type notation as $P=\bbnum 1+\left(\bbnum 1+\bbnum 2\rightarrow\bbnum 2\right)$
and find 
\[
\left|P\right|=\left|\bbnum 1+\left(\bbnum 1+\bbnum 2\rightarrow\bbnum 2\right)\right|=1+\left|\bbnum 1+\bbnum 2\rightarrow\bbnum 2\right|=1+8=9\quad.
\]


\subsubsection{Example \label{subsec:ch-solvedExample-2}\ref{subsec:ch-solvedExample-2}}

Implement a Scala type \lstinline!P[A]! for the type notation 
\[
P^{A}\triangleq1+A+\text{Int}\times A+(\text{String}\rightarrow A)\quad.
\]


\subparagraph{Solution}

To translate type notation into Scala code, begin by defining the
disjunctive types as case classes (with names chosen for convenience).
In this case, $P^{A}$ is a disjunctive type with four parts, so we
will need four case classes:
\begin{lstlisting}
sealed trait P[A]
final case class P1[A](???) extends P[A]
final case class P2[A](???) extends P[A]
final case class P3[A](???) extends P[A]
final case class P4[A](???) extends P[A]
\end{lstlisting}
Each of the case classes represents one part of the disjunctive type.
Now we write the contents for each of the case classes, in order to
implement the data in each of the disjunctive parts:
\begin{lstlisting}
sealed trait P[A]
final case class P1[A]()               extends P[A]
final case class P2[A](x: A)           extends P[A]
final case class P3[A](n: Int, x: A)   extends P[A]
final case class P4[A](f: String => A) extends P[A]
\end{lstlisting}


\subsubsection{Example \label{subsec:ch-solvedExample-2a}\ref{subsec:ch-solvedExample-2a}}

Find an equivalent disjunctive type for the type \lstinline!P = (Either[A, B], Either[C, D])!.

\subparagraph{Solution}

Begin by writing the given type in the type notation. The tuple becomes
the product type, and \lstinline!Either! becomes the disjunctive
(or \textsf{``}sum\textsf{''}) type:
\[
P\triangleq(A+B)\times(C+D)\quad.
\]
We can use the usual rules of arithmetic to expand brackets in this
type expression and to obtain an equivalent type:
\[
P\cong A\times C+A\times D+B\times C+B\times D\quad.
\]
This is a disjunctive type having $4$ parts.

\subsubsection{Example \label{subsec:ch-solvedExample-3}\ref{subsec:ch-solvedExample-3}}

Show that the following type equivalences do \emph{not} hold: $A+A\not\cong A$
and $A\times A\not\cong A$, although the corresponding logical identities
hold.

\subparagraph{Solution}

Note that the arithmetic equalities do not hold, $A+A\neq A$ and
$A\times A\ne A$. This already indicates that the types are not equivalent.
To build further intuition, consider that a value of type $A+A$ (in
Scala, \lstinline!Either[A, A]!) is a \lstinline!Left(a)! or a \lstinline!Right(a)!
for some \lstinline!a:A!. In the code notation, it is either $a^{:A}+\bbnum 0$
or $\bbnum 0+a^{:A}$. So, a value of type $A+A$ contains a value
of type $A$ with the additional information about whether it is the
first or the second part of the disjunctive type. We cannot represent
that information in a single value of type $A$. 

Similarly, a value of type $A\times A$ contains two (possibly different)
values of type $A$, which cannot be represented by a single value
of type $A$ without loss of information.

However, the corresponding logical identities $\alpha\vee\alpha=\alpha$
and $\alpha\wedge\alpha=\alpha$ hold. To see that, we could derive
the four formulas
\begin{align*}
\alpha\vee\alpha\Rightarrow\alpha\quad, & \quad\quad\alpha\Rightarrow\alpha\vee\alpha\quad,\\
\alpha\wedge\alpha\Rightarrow\alpha\quad, & \quad\quad\alpha\Rightarrow\alpha\wedge\alpha\quad,
\end{align*}
using the proof rules of Section~\ref{subsec:The-rules-of-proof}.
Alternatively, we may use the CH correspondence and show that the
type signatures
\begin{align*}
\forall A.\,A+A\rightarrow A\quad, & \quad\quad\forall A.\,A\rightarrow A+A\quad,\\
\forall A.\,A\times A\rightarrow A\quad, & \quad\quad\forall A.\,A\rightarrow A\times A\quad
\end{align*}
can be implemented via fully parametric functions. For a programmer,
it is easier to write code than to guess the correct sequence of proof
rules. For the first pair of type signatures, we find
\begin{lstlisting}
def f1[A]: Either[A, A] => A = {
  case Left(a)    => a   // No other choice here.
  case Right(a)   => a   // No other choice here.
}
def f2[A]: A => Either[A, A] = { a => Left(a) } // Can be also Right(a).
\end{lstlisting}
The presence of an arbitrary choice, to return \lstinline!Left(a)!
or \lstinline!Right(a)!, is a warning sign showing that additional
information is required to create a value of type \lstinline!Either[A, A]!.
This is precisely the information present in the type $A+A$ but missing
in the type $A$.

The code notation for these functions is
\[
f_{1}\triangleq\,\begin{array}{|c||c|}
 & A\\
\hline A & a\rightarrow a\\
A & a\rightarrow a
\end{array}\,=\,\begin{array}{|c||c|}
 & A\\
\hline A & \text{id}\\
A & \text{id}
\end{array}\quad,\quad\quad f_{2}\triangleq a^{:A}\rightarrow a+\bbnum 0^{:A}=\,\begin{array}{|c||cc|}
 & A & A\\
\hline A & a\rightarrow a & \bbnum 0
\end{array}\,=\,\begin{array}{|c||cc|}
 & A & A\\
\hline A & \text{id} & \bbnum 0
\end{array}\quad.
\]
The composition of these functions is not equal to identity:
\[
f_{1}\bef f_{2}=\,\begin{array}{||c|}
\text{id}\\
\text{id}
\end{array}\,\bef\,\begin{array}{||cc|}
\text{id} & \bbnum 0\end{array}\,=\,\begin{array}{||cc|}
\text{id} & \bbnum 0\\
\text{id} & \bbnum 0
\end{array}\,\neq\text{id}=\,\begin{array}{||cc|}
\text{id} & \bbnum 0\\
\bbnum 0 & \text{id}
\end{array}\quad.
\]

For the second pair of type signatures, the code is
\begin{lstlisting}
def f1[A]: ((A, A)) => A = { case (a1, a2) => a1 }   // Can be also `a2`.
cef f2[A]:   A => (A, A) = { a => (a, a) }           // No other choice here.
\end{lstlisting}
It is clear that the first function loses information when it returns
\lstinline!a1! and discards \lstinline!a2! (or vice versa).

The code notation for the functions \lstinline!f1! and \lstinline!f2!
is
\[
f_{1}\triangleq a_{1}^{:A}\times a_{2}^{:A}\rightarrow a_{1}=\pi_{1}^{:A\times A\rightarrow A}\quad,\quad\quad f_{2}\triangleq a^{:A}\rightarrow a\times a=\Delta^{:A\rightarrow A\times A}\quad.
\]
Computing the compositions of these functions, we find that $f_{2}\bef f_{1}=\text{id}$
while $f_{1}\bef f_{2}\ne\text{id}$:
\begin{align*}
f_{1}\bef f_{2} & =\left(a_{1}\times a_{2}\rightarrow a_{1}\right)\bef\left(a\rightarrow a\times a\right)\\
 & =\left(a_{1}\times a_{2}\rightarrow a_{1}\times a_{1}\right)\neq\text{id}=\left(a_{1}\times a_{2}\rightarrow a_{1}\times a_{2}\right)\quad.
\end{align*}

We have implemented all four type signatures as fully parametric functions,
which shows that the corresponding logical formulas are all true (i.e.,
can be derived using the proof rules). However, the functions cannot
be inverses of each other. So, the type equivalences do not hold.

\subsubsection{Example \label{subsec:ch-solvedExample-4}\ref{subsec:ch-solvedExample-4}}

Show that $\left(\left(A\wedge B\right)\Rightarrow C\right)\neq(A\Rightarrow C)\vee(B\Rightarrow C)$
in the constructive logic, but the equality holds in Boolean logic.
(This is another example where Boolean reasoning about types fails.)

\subparagraph{Solution}

Begin by rewriting the logical equality as two implications,
\[
(A\wedge B\Rightarrow C)\Rightarrow(A\Rightarrow C)\vee(B\Rightarrow C)\quad\text{ and }\quad\left((A\Rightarrow C)\vee(B\Rightarrow C)\right)\Rightarrow\left(\left(A\wedge B\right)\Rightarrow C\right)\quad.
\]
It is sufficient to show that one of these implications is incorrect.
Rather than looking for a proof tree in the constructive logic (which
would be difficult, since we would need to demonstrate that \emph{no}
proof tree exists), let us use the CH correspondence. So the task
is to implement fully parametric functions with the type signatures
\[
(A\times B\rightarrow C)\rightarrow(A\rightarrow C)+(B\rightarrow C)\quad\text{ and }\quad(A\rightarrow C)+(B\rightarrow C)\rightarrow A\times B\rightarrow C\quad.
\]
For the first type signature, the Scala code is
\begin{lstlisting}
def f1[A,B,C]: (((A, B)) => C) => Either[A => C, B => C] = { k => ??? }
\end{lstlisting}
We are required to return either a \lstinline!Left(g)! with \lstinline!g: A => C!,
or a \lstinline!Right(h)! with \lstinline!h: B => C!. The only given
data is a function \lstinline!k! of type $A\times B\rightarrow C$,
so the decision of whether to return a \lstinline!Left! or a \lstinline!Right!
must be hard-coded in the function \lstinline!f1! independently of
\lstinline!k!. Can we produce a function \lstinline!g! of type \lstinline!A => C!?
Given a value of type \lstinline!A!, we would need to return a value
of type \lstinline!C!. The only way to obtain a value of type \lstinline!C!
is by applying \lstinline!k! to some arguments. But to apply \lstinline!k!,
we need a value of type \lstinline!B!, which we do not have. So we
cannot produce a \lstinline!g: A => C!. Similarly, we cannot produce
a function \lstinline!h! of type \lstinline!B => C!.

To repeat the same argument in the type notation: Obtaining a value
of type $(A\rightarrow C)+(B\rightarrow C)$ means to compute either
$g^{:A\rightarrow C}+\bbnum 0$ or $\bbnum 0+h^{:B\rightarrow C}$.
This decision must be hard-coded since the only data is a function
$k^{:A\times B\rightarrow C}$. We can compute $g^{:A\rightarrow C}$
only by partially applying $k^{:A\times B\rightarrow C}$ to a value
of type $B$. However, we have no values of type $B$. Similarly,
we cannot get an $h^{:B\rightarrow C}$.

The inverse type signature \emph{can} be implemented:

\begin{wrapfigure}{l}{0.55\columnwidth}%
\vspace{0.32\baselineskip}
\begin{lstlisting}
def f2[A,B,C]: Either[A=>C, B=>C] => ((A,B)) => C = {
  case Left(g)    =>   { case (a, b)    => g(a) }
  case Right(h)   =>   { case (a, b)    => h(b) }
}
\end{lstlisting}

\vspace{-2.4\baselineskip}
\end{wrapfigure}%
\vspace{-1.2\baselineskip}

\noindent 
\[
f_{2}\triangleq\,\begin{array}{|c||c|}
 & A\times B\rightarrow C\\
\hline A\rightarrow C & g^{:A\rightarrow C}\rightarrow a\times b\rightarrow g(a)\\
B\rightarrow C & h^{:B\rightarrow C}\rightarrow a\times b\rightarrow h(b)
\end{array}\quad.
\]
\vspace{-0.9\baselineskip}

Let us now show that the logical identity 
\begin{equation}
((\alpha\wedge\beta)\Rightarrow\gamma)=((\alpha\Rightarrow\gamma)\vee(\beta\Rightarrow\gamma))\label{eq:ch-example-identity-boolean-not-constructive}
\end{equation}
holds in Boolean logic. A straightforward calculation is to simplify
the Boolean expression using Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic}),
which only holds in Boolean logic (but not in the constructive logic).
We find
\begin{align*}
{\color{greenunder}\text{left-hand side of Eq.~(\ref{eq:ch-example-identity-boolean-not-constructive})}:}\quad & \left(\alpha\wedge\beta\right)\gunderline{\Rightarrow}\,\gamma\\
{\color{greenunder}\text{use Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & \quad=\gunderline{\neg(\alpha\wedge\beta)}\vee\gamma\\
{\color{greenunder}\text{use de Morgan\textsf{'}s law}:}\quad & \quad=\neg\alpha\vee\neg\beta\vee\gamma\quad.\\
{\color{greenunder}\text{right-hand side of Eq.~(\ref{eq:ch-example-identity-boolean-not-constructive})}:}\quad & (\gunderline{\alpha\Rightarrow\gamma})\vee(\gunderline{\beta\Rightarrow\gamma})\\
{\color{greenunder}\text{use Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & \quad=\neg\alpha\vee\gunderline{\gamma}\vee\neg\beta\vee\gunderline{\gamma}\\
{\color{greenunder}\text{use identity }\gamma\vee\gamma=\gamma:}\quad & \quad=\neg\alpha\vee\neg\beta\vee\gamma\quad.
\end{align*}
Both sides of Eq.~(\ref{eq:ch-example-identity-boolean-not-constructive})
are equal to the same formula, $\neg\alpha\vee\neg\beta\vee\gamma$,
so the identity holds.

This calculation does not work in the constructive logic because its
proof rules can derive neither the Boolean formula~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})
nor the \textbf{law of de Morgan}\index{law of de Morgan}, $\neg(\alpha\wedge\beta)=\left(\neg\alpha\vee\neg\beta\right)$.

Another way of proving the Boolean identity~(\ref{eq:ch-example-identity-boolean-not-constructive})
is to enumerate all possible truth values for the variables $\alpha$,
$\beta$, and $\gamma$. The left-hand side, $\left(\alpha\wedge\beta\right)\Rightarrow\gamma$,
can be $False$ only if $\alpha\wedge\beta=True$ (that is, both $\alpha$
and $\beta$ are $True$) and $\gamma=False$; for all other truth
values of $\alpha$, $\beta$, and $\gamma$, the formula $\left(\alpha\wedge\beta\right)\Rightarrow\gamma$
is $True$. Let us determine when the right-hand side, $(\alpha\Rightarrow\gamma)\vee(\beta\Rightarrow\gamma)$,
can be $False$. This can happen only if both parts of the disjunction
are $False$; that means $\alpha=True$, $\beta=True$, and $\gamma=False$.
So, the two sides of the identity~(\ref{eq:ch-example-identity-boolean-not-constructive})
are both $True$ or both $False$ with any choice of truth values
of $\alpha$, $\beta$, and $\gamma$. In Boolean logic, this is sufficient
to prove the identity~(\ref{eq:ch-example-identity-boolean-not-constructive}).

It is important to note that the proof rules of the constructive logic
are not equivalent to checking whether some propositions are $True$
or $False$. A general form of this statement was proved by Kurt G\"odel\index{Kurt@Kurt G\"odel}
in 1932.\footnote{See \texttt{\href{https://plato.stanford.edu/entries/intuitionistic-logic-development/\#SomeEarlResu}{plato.stanford.edu/entries/intuitionistic-logic-development/}}}
In this sense, constructive logic does not imply that every proposition
is either $True$ or $False$. This is not intuitive and requires
getting used to.

The following example shows how to use the identities from Tables~\ref{tab:Logical-identities-with-disjunction-and-conjunction}\textendash \ref{tab:Logical-identities-with-function-types}
to derive type equivalence for complicated type expressions, without
need for proofs.

\subsubsection{Example \label{subsec:ch-solvedExample-5-2}\ref{subsec:ch-solvedExample-5-2}}

Use known rules to verify the type equivalences:

\textbf{(a)} $A\times\left(A+\bbnum 1\right)\times\left(A+\bbnum 1+\bbnum 1\right)\cong A\times\left(\bbnum 1+\bbnum 1+A\times\left(\bbnum 1+\bbnum 1+\bbnum 1+A\right)\right)$.

\textbf{(b)} $\bbnum 1+A+B\rightarrow\bbnum 1\times B\cong\left(B\rightarrow B\right)\times\left(A\rightarrow B\right)\times B$.

\subparagraph{Solution}

\textbf{(a)} We can expand brackets in the type expression as in arithmetic,
\begin{align*}
A\times\left(A+\bbnum 1\right) & \cong A\times A+A\times\bbnum 1\cong A\times A+A\quad,\\
A\times\left(A+\bbnum 1\right)\times\left(A+\bbnum 1+\bbnum 1\right) & \cong\left(A\times A+A\right)\times\left(A+\bbnum 1+\bbnum 1\right)\\
 & \cong A\times A\times A+A\times A+A\times A\times\left(\bbnum 1+\bbnum 1\right)+A\times\left(\bbnum 1+\bbnum 1\right)\\
 & \cong A\times A\times A+A\times A\times\left(\bbnum 1+\bbnum 1+\bbnum 1\right)+A\times\left(\bbnum 1+\bbnum 1\right)\quad.
\end{align*}
The result looks like a polynomial in $A$, which we can now rearrange
into the required form:
\[
A\times A\times A+A\times A\times\left(\bbnum 1+\bbnum 1+\bbnum 1\right)+A\times\left(\bbnum 1+\bbnum 1\right)\cong A\times\left(\bbnum 1+\bbnum 1+A\times\left(\bbnum 1+\bbnum 1+\bbnum 1+A\right)\right)\quad.
\]

\textbf{(b)} Keep in mind that the conventions of the type notation
make the function arrow $\left(\rightarrow\right)$ group weaker than
other type operations. So, the type expression $\bbnum 1+A+B\rightarrow\bbnum 1\times B$
means a function from $\bbnum 1+A+B$ to $\bbnum 1\times B$. 

Begin by using the rule $\bbnum 1\times B\cong B$ to obtain $\bbnum 1+A+B\rightarrow B$.
Now we use the rule 
\[
A+B\rightarrow C\cong\left(A\rightarrow C\right)\times\left(B\rightarrow C\right)
\]
and derive the equivalence
\[
\bbnum 1+A+B\rightarrow B\cong\left(\bbnum 1\rightarrow B\right)\times\left(A\rightarrow B\right)\times\left(B\rightarrow B\right)\quad.
\]
Finally, we note that $\bbnum 1\rightarrow B\cong B$ and that the
type product is commutative, so we can rearrange the last type expression
into the required form:
\[
B\times\left(A\rightarrow B\right)\times\left(B\rightarrow B\right)\cong\left(B\rightarrow B\right)\times\left(A\rightarrow B\right)\times B\quad.
\]


\subsubsection{Example \label{subsec:ch-solvedExample-5}\ref{subsec:ch-solvedExample-5}}

Denote $\text{Read}^{E,T}\triangleq E\rightarrow T$ and implement
fully parametric functions with types $A\rightarrow\text{Read}^{E,A}$
and $\text{Read}^{E,A}\rightarrow(A\rightarrow B)\rightarrow\text{Read}^{E,B}$.

\subparagraph{Solution}

Begin by defining a type alias for the type constructor $\text{Read}^{E,T}$:
\begin{lstlisting}
type Read[E, T] = E => T
\end{lstlisting}
The first type signature has only one implementation:
\begin{lstlisting}
def p[E, A]: A => Read[E, A] = { x => _ => x }
\end{lstlisting}
We \emph{must} discard the argument of type $E$; we cannot use it
for computing a value of type \lstinline!A! given \lstinline!x:A!.

The second type signature has three type parameters. It is the curried
version of the function \lstinline!map!:
\begin{lstlisting}
def map[E, A, B]: Read[E, A] => (A => B) => Read[E, B] = ???
\end{lstlisting}
Expanding the type alias, we see that the two curried arguments are
functions of types $E\rightarrow A$ and $A\rightarrow B$. The forward
composition of these functions is a function of type $E\rightarrow B$,
or $\text{Read}^{E,B}$, which is exactly what we are required to
return. So the code can be written as

\begin{lstlisting}
def map[E, A, B]: (E => A) => (A => B) => E => B = { r => f => r andThen f }
\end{lstlisting}
If we did not notice this shortcut, we would reason differently: We
are required to compute a value of type $B$ given \emph{three} curried
arguments $r^{:E\rightarrow A}$, $f^{:A\rightarrow B}$, and $e^{:E}$.
Write this requirement as
\[
\text{map}\triangleq r^{:E\rightarrow A}\rightarrow f^{:A\rightarrow B}\rightarrow e^{:E}\rightarrow???^{:B}\quad,
\]
The symbol $\text{???}^{:B}$ is called a \index{typed hole}\textbf{typed
hole}; it stands for a value that we are still figuring out how to
compute, but whose type is already known. Typed holes are supported
in Scala by an experimental compiler plugin.\footnote{\texttt{\href{https://github.com/cb372/scala-typed-holes}{https://github.com/cb372/scala-typed-holes}}}
The plugin will print the known information about the typed hole.

To fill the typed hole $\text{???}^{:B}$, we need a value of type
$B$. Since no arguments have type $B$, the only way of getting a
value of type $B$ is to apply $f^{:A\rightarrow B}$ to some value
of type $A$. So we write
\[
\text{map}\triangleq r^{:E\rightarrow A}\rightarrow f^{:A\rightarrow B}\rightarrow e^{:E}\rightarrow f(???^{:A})\quad.
\]
The only way of getting an $A$ is to apply $r$ to a value of type
$E$,
\[
\text{map}\triangleq r^{:E\rightarrow A}\rightarrow f^{:A\rightarrow B}\rightarrow e^{:E}\rightarrow f(r(???^{:E}))\quad.
\]
We have exactly one value of type $E$, namely $e^{:E}$. So the code
must be 
\[
\text{map}^{E,A,B}\triangleq r^{:E\rightarrow A}\rightarrow f^{:A\rightarrow B}\rightarrow e^{:E}\rightarrow f(r(e))\quad.
\]
Translate this to the Scala syntax:
\begin{lstlisting}
def map[E, A, B]: (E => A) => (A => B) => E => B = { r => f => e => f(r(e)) }
\end{lstlisting}
We may now notice that the expression $e\rightarrow f(r(e))$ is a
function composition $r\bef f$ applied to $e$, and simplify the
code accordingly.

\subsubsection{Example \label{subsec:ch-solvedExample-6}\ref{subsec:ch-solvedExample-6}}

Show that the type signature \lstinline!Read[A, T] => (A => B) => Read[B, T]!
cannot be implemented as a fully parametric function.

\subparagraph{Solution}

Expand the type signature and try implementing this function:
\begin{lstlisting}
def m[A, B, T] : (A => T) => (A => B) => B => T = { r => f => b => ??? }
\end{lstlisting}
Given values $r^{:A\rightarrow T}$, $f^{:A\rightarrow B}$, and $b^{:B}$,
we need to compute a value of type $T$:
\[
m=r^{:A\rightarrow T}\rightarrow f^{:A\rightarrow B}\rightarrow b^{:B}\rightarrow???^{:T}\quad.
\]
The only way of getting a value of type $T$ is to apply $r$ to some
value of type $A$,
\[
m=r^{:A\rightarrow T}\rightarrow f^{:A\rightarrow B}\rightarrow b^{:B}\rightarrow r(???^{:A})\quad.
\]
However, we do not have any values of type $A$. We have a function
$f^{:A\rightarrow B}$ that \emph{consumes} values of type $A$, and
we cannot use $f$ to produce any values of type $A$. So we seem
to be unable to fill the typed hole $\text{???}^{:A}$ and implement
the function \lstinline!m!.

In order to verify that \lstinline!m! is unimplementable, we need
to prove that the logical formula
\begin{equation}
\forall(\alpha,\beta,\tau).\,(\alpha\Rightarrow\tau)\Rightarrow(\alpha\Rightarrow\beta)\Rightarrow(\beta\Rightarrow\tau)\label{eq:ch-example-boolean-formula-3}
\end{equation}
is not true in the constructive logic. We could use the \texttt{curryhoward}
library for that:
\begin{lstlisting}
@ def m[A, B, T] : (A => T) => (A => B) => B => T = implement
cmd1.sc:1: type (A => T) => (A => B) => B => T cannot be implemented
def m[A, B, T] : (A => T) => (A => B) => B => T = implement
                                                ^
Compilation Failed
\end{lstlisting}
Another way is to check whether this formula is true in Boolean logic.
A formula that holds in constructive logic will always hold in Boolean
logic, because all rules shown in Section~\ref{subsec:The-rules-of-proof}
preserve Boolean truth values (see Section~\ref{subsec:Relationship-between-Boolean}
for a proof). It follows that any formula that fails to hold in Boolean
logic will also not hold in constructive logic. 

It is relatively easy to check whether a given Boolean formula is
always equal to $True$. Simplifying Eq.~(\ref{eq:ch-example-boolean-formula-3})
with the rules of Boolean logic, we find
\begin{align*}
 & (\alpha\Rightarrow\tau)\,\gunderline{\Rightarrow}\,(\alpha\Rightarrow\beta)\,\gunderline{\Rightarrow}\,(\beta\Rightarrow\tau)\\
{\color{greenunder}\text{use Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & =\neg(\gunderline{\alpha\Rightarrow\tau})\vee\neg(\gunderline{\alpha\Rightarrow\beta})\vee(\gunderline{\beta\Rightarrow\tau})\\
{\color{greenunder}\text{use Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & =\gunderline{\neg(\neg\alpha\vee\tau)}\vee\gunderline{\neg(\neg\alpha\vee\beta)}\vee(\neg\beta\vee\tau)\\
{\color{greenunder}\text{use de Morgan\textsf{'}s law}:}\quad & =\left(\alpha\wedge\neg\tau\right)\vee\gunderline{\left(\alpha\wedge\neg\beta\right)\vee\neg\beta}\vee\tau\\
{\color{greenunder}\text{use identity }(p\wedge q)\vee q=q:}\quad & =\gunderline{\left(\alpha\wedge\neg\tau\right)}\vee\neg\beta\vee\gunderline{\tau}\\
{\color{greenunder}\text{use identity }(p\wedge\neg q)\vee q=p\vee q:}\quad & =\alpha\vee\neg\beta\vee\tau\quad.
\end{align*}
This formula is not identically $True$: it is $False$ when $\alpha=\tau=False$
and $\beta=True$. So, Eq.~(\ref{eq:ch-example-boolean-formula-3})
is not true in Boolean logic, and thus is not true in constructive
logic. By the CH correspondence, we conclude that the type signature
of \lstinline!m! cannot be implemented by a fully parametric function.

\subsubsection{Example \label{subsec:ch-solvedExample-7}\ref{subsec:ch-solvedExample-7}}

Define the type constructor $P^{A}\triangleq\bbnum 1+A+A$ and implement
\lstinline!map! for it,
\[
\text{map}^{A,B}:P^{A}\rightarrow(A\rightarrow B)\rightarrow P^{B}\quad.
\]
To check that \lstinline!map! preserves information, verify the law
\lstinline!map(p)(x => x) == p! for all \lstinline!p: P[A]!.

\subparagraph{Solution}

It is implied that \lstinline!map! should be fully parametric and
information-preserving. Begin by defining a Scala type constructor
for the notation $P^{A}\triangleq\bbnum 1+A+A$:
\begin{lstlisting}
sealed trait P[A]
final case class P1[A]()     extends P[A]
final case class P2[A](x: A) extends P[A]
final case class P3[A](x: A) extends P[A]
\end{lstlisting}
Now we can write code to implement the required type signature. Each
time we have several choices of an implementation, we will choose
to preserve information as much as possible.

\begin{wrapfigure}{l}{0.45\columnwidth}%
\vspace{0.24\baselineskip}

\begin{lstlisting}
def map[A, B]: P[A] => (A => B) => P[B] =
  p => f => p match {
    case P1() => P1() // No other choice.
    case P2(x) => ???
    case P3(x) => ???
  }
\end{lstlisting}
\vspace{-0.9\baselineskip}
\end{wrapfigure}%

\noindent In the case \lstinline!P2(x)!, we are required to produce
a value of type $P^{B}$ from a value $x^{:A}$ and a function $f^{:A\rightarrow B}$.
Since $P^{B}$ is a disjunctive type with three parts, we can produce
a value of type $P^{B}$ in three different ways: \lstinline!P1()!,
\lstinline!P2(...)!, and \lstinline!P3(...)!. If we return \lstinline!P1()!,
we will lose the information about the value \lstinline!x!. If we
return \lstinline!P3(...)!, we will preserve the information about
\lstinline!x! but lose the information\index{information loss} that
the input value was a \lstinline!P2! rather than a \lstinline!P3!.
By returning \lstinline!P2(...)! in that scope, we preserve the entire
input information. 

The value under \lstinline!P2(...)! must be of type $B$, and the
only way of getting a value of type $B$ is to apply $f$ to $x$.
So, we return \lstinline!P2(f(x))!.

Similarly, in the case \lstinline!P3(x)!, we should return \lstinline!P3(f(x))!.
The final code of \lstinline!map! is
\begin{lstlisting}
def map[A, B]: P[A] => (A => B) => P[B] = p => f => p match {
  case P1() => P1()         // No other choice here.
  case P2(x) => P2(f(x))    // Preserve information.
  case P3(x) => P3(f(x))    // Preserve information.
}
\end{lstlisting}

To verify the given law, we first write a matrix notation for \lstinline!map!:
\[
\text{map}^{A,B}\triangleq p^{:\bbnum 1+A+A}\rightarrow f^{:A\rightarrow B}\rightarrow p\triangleright\,\begin{array}{|c||ccc|}
 & \bbnum 1 & B & B\\
\hline \bbnum 1 & \text{id} & \bbnum 0 & \bbnum 0\\
A & \bbnum 0 & f & \bbnum 0\\
A & \bbnum 0 & \bbnum 0 & f
\end{array}\quad.
\]
The required law is written as an equation (called the\index{identity laws!of map@of \texttt{map}}
\textbf{identity law})
\[
\text{map}\left(p\right)(\text{id})=p\quad.
\]
Substituting the code notation for \lstinline!map!, we verify the
law:
\begin{align*}
{\color{greenunder}\text{expect to equal }p:}\quad & \text{map}\left(p\right)(\text{id})\\
{\color{greenunder}\text{apply map()() to arguments}:}\quad & =p\triangleright\,\begin{array}{||ccc|}
\text{id} & \bbnum 0 & \bbnum 0\\
\bbnum 0 & \text{id} & \bbnum 0\\
\bbnum 0 & \bbnum 0 & \text{id}
\end{array}\\
{\color{greenunder}\text{identity function in matrix notation}:}\quad & =p\triangleright\text{id}\\
{\color{greenunder}\triangleright\text{-notation}:}\quad & =\text{id}\left(p\right)=p\quad.
\end{align*}


\subsubsection{Example \label{subsec:ch-solvedExample-8}\ref{subsec:ch-solvedExample-8}}

Implement \lstinline!map! and \lstinline!flatMap! for \lstinline!Either[L, R]!,
applied to the type parameter \lstinline!L!.

\subparagraph{Solution}

For a type constructor, say, $P^{A}$, the standard type signatures
for \lstinline!map! and \lstinline!flatMap! are
\begin{align*}
\text{map} & :P^{A}\rightarrow(A\rightarrow B)\rightarrow P^{B}\quad,\\
\text{flatMap} & :P^{A}\rightarrow(A\rightarrow P^{B})\rightarrow P^{B}\quad.
\end{align*}
If a type constructor has more than one type parameter, e.g., $P^{A,S,T}$,
one can define the functions \lstinline!map! and \lstinline!flatMap!
applied to a chosen type parameter. For example, when applied to the
type parameter $A$, the type signatures are 
\begin{align*}
\text{map} & :P^{A,S,T}\rightarrow(A\rightarrow B)\rightarrow P^{B,S,T}\quad,\\
\text{flatMap} & :P^{A,S,T}\rightarrow(A\rightarrow P^{B,S,T})\rightarrow P^{B,S,T}\quad.
\end{align*}
Being \textsf{``}applied to the type parameter $A$\textsf{''} means that the other
type parameters $S,T$ in $P^{A,S,T}$ remain fixed while the type
parameter $A$ is replaced by $B$ in the type signatures of \lstinline!map!
and \lstinline!flatMap!.

For the type \lstinline!Either[L, R]! (i.e., $L+R$), we keep the
type parameter $R$ fixed while $L$ is replaced by $M$. So we obtain
the type signatures
\begin{align*}
\text{map} & :L+R\rightarrow(L\rightarrow M)\rightarrow M+R\quad,\\
\text{flatMap} & :L+R\rightarrow(L\rightarrow M+R)\rightarrow M+R\quad.
\end{align*}
Implementing these functions is straightforward:
\begin{lstlisting}
def map[L,M,R]: Either[L, R] => (L => M) => Either[M, R] = e => f => e match {
  case Left(x)    => Left(f(x))
  case Right(y)   => Right(y)
}
def flatMap[L,M,R]: Either[L, R] => (L => Either[M, R]) => Either[M, R] = e => f => e match {
  case Left(x)    => f(x)
  case Right(y)   => Right(y)
}
\end{lstlisting}
The code notation for these functions is
\begin{align*}
\text{map} & \triangleq e^{:L+R}\rightarrow f^{:L\rightarrow M}\rightarrow e\triangleright\,\begin{array}{|c||cc|}
 & M & R\\
\hline L & f & \bbnum 0\\
R & \bbnum 0 & \text{id}
\end{array}\quad,\\
\text{flatMap} & \triangleq e^{:L+R}\rightarrow f^{:L\rightarrow M+R}\rightarrow e\triangleright\,\begin{array}{|c||c|}
 & M+R\\
\hline L & f\\
R & y^{:R}\rightarrow\bbnum 0^{:M}+y
\end{array}\quad.
\end{align*}
Note that we cannot split $f$ into the $M$ and $R$ columns since
$f(x^{:L})$ could return either part of the disjunctive type $M+R$.

\subsubsection{Example \label{subsec:ch-solvedExample-9}\ref{subsec:ch-solvedExample-9}{*}}

Define a type constructor $\text{State}^{S,A}\equiv S\rightarrow A\times S$
and implement the functions:

\textbf{(a)} $\text{pure}^{S,A}:A\rightarrow\text{State}^{S,A}\quad.$

\textbf{(b)} $\text{map}^{S,A,B}:\text{State}^{S,A}\rightarrow(A\rightarrow B)\rightarrow\text{State}^{S,B}\quad.$

\textbf{(c)} $\text{flatMap}^{S,A,B}:\text{State}^{S,A}\rightarrow(A\rightarrow\text{State}^{S,B})\rightarrow\text{State}^{S,B}\quad.$

\subparagraph{Solution}

It is assumed that all functions must be fully parametric and preserve
as much information as possible. We define the type alias
\begin{lstlisting}
type State[S, A] = S => (A, S)
\end{lstlisting}

\textbf{(a)} The type signature is $A\rightarrow S\rightarrow A\times S$,
and there is only one implementation,
\begin{lstlisting}
def pure[S, A]: A => State[S, A] = a => s => (a, s)
\end{lstlisting}
In the code notation, this is written as
\[
\text{pu}^{S,A}\triangleq a^{:A}\rightarrow s^{:S}\rightarrow a\times s\quad.
\]

\textbf{(b)} The type signature is 
\[
\text{map}^{S,A,B}:(S\rightarrow A\times S)\rightarrow(A\rightarrow B)\rightarrow S\rightarrow B\times S\quad.
\]
Begin writing a Scala implementation:
\begin{lstlisting}
def map[S, A, B]: State[S, A] => (A => B) => State[S, B] = { t => f => s => ??? }
\end{lstlisting}
We need to compute a value of $B\times S$ from the curried arguments
$t^{:S\rightarrow A\times S}$, $f^{:A\rightarrow B}$, and $s^{:S}$.
We begin writing the code of \lstinline!map! using a typed hole,
\[
\text{map}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow B}\rightarrow s^{:S}\rightarrow\text{???}^{:B}\times\text{???}^{:S}\quad.
\]
The only way of getting a value of type $B$ is by applying $f$ to
a value of type $A$:
\[
\text{map}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow B}\rightarrow s^{:S}\rightarrow f(\text{???}^{:A})\times\text{???}^{:S}\quad.
\]
The only possibility of filling the typed hole $\text{???}^{:A}$
is to apply $t$ to a value of type $S$; we already have such a value,
$s^{:S}$. Computing $t(s)$ yields a pair of type $A\times S$, from
which we may take the first part (of type $A$) to fill the typed
hole $\text{???}^{:A}$. The second part of the pair is a value of
type $S$ that we may use to fill the second typed hole, $\text{???}^{:S}$.
So the Scala code is

\begin{wrapfigure}{l}{0.62\columnwidth}%
\vspace{-0.9\baselineskip}
\begin{lstlisting}[numbers=left]
def map[S, A, B]: State[S, A] => (A => B) => State[S, B] = {
  t => f => s =>
    val (a, s2) = t(s)
    (f(a), s2)     // We could also return `(f(a), s)` here.
}
\end{lstlisting}
\vspace{-1.25\baselineskip}
\end{wrapfigure}%

\noindent Why not return the original value \lstinline!s! in the
tuple $B\times S$, instead of the new value \lstinline!s2!? The
reason is that we would like to preserve information as much as possible.
If we return \lstinline!(f(a), s)! in line 4, we will have discarded
the computed value \lstinline!s2!, which is a loss of information.

To write the code notation for \lstinline!map!, we need to destructure
the pair that $t(s)$ returns. We can write explicit destructuring
code like this:
\[
\text{map}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow B}\rightarrow s^{:S}\rightarrow(a^{:A}\times s_{2}^{:S}\rightarrow f(a)\times s_{2})(t(s))\quad.
\]
If we temporarily denote by $q$ the destructuring function 
\[
q\triangleq(a^{:A}\times s_{2}^{:S}\rightarrow f(a)\times s_{2})\quad,
\]
we will notice that the expression $s\rightarrow q(t(s))$ is a function
composition applied to $s$. So, we rewrite $s\rightarrow q(t(s))$
as the composition $t\bef q$ and obtain shorter code, 
\[
\text{map}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow B}\rightarrow t\bef(a^{:A}\times s^{:S}\rightarrow f(a)\times s)\quad.
\]
Shorter formulas are often easier to reason about in derivations (although
not necessarily easier to read when converted to program code).

\textbf{(c)} The required type signature is
\[
\text{flatMap}^{S,A,B}:(S\rightarrow A\times S)\rightarrow(A\rightarrow S\rightarrow B\times S)\rightarrow S\rightarrow B\times S\quad.
\]
We perform code reasoning with typed holes:
\[
\text{flatMap}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow S\rightarrow B\times S}\rightarrow s^{:S}\rightarrow\text{???}^{:B}\times???^{:S}\quad.
\]
To fill $\text{???}^{:B}$, we need to apply $f$ to some arguments,
since $f$ is the only function that returns any values of type $B$.
A saturated application of $f$ will yield a value of type $B\times S$,
which we can return without change:
\[
\text{flatMap}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow S\rightarrow B\times S}\rightarrow s^{:S}\rightarrow f(\text{???}^{:A})(\text{???}^{:S})\quad.
\]
To fill the new typed holes, we need to apply $t$ to an argument
of type $S$. We have only one given value $s^{:S}$ of type $S$,
so we must compute $t(s)$ and destructure it:
\[
\text{flatMap}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow S\rightarrow B\times S}\rightarrow s^{:S}\rightarrow\left(a\times s_{2}\rightarrow f(a)(s_{2})\right)(t(s))\quad.
\]
Translating this notation into Scala code, we obtain
\begin{lstlisting}
def flatMap[S, A, B]: State[S, A] => (A => State[S, B]) => State[S, B] = {
  t => f => s =>
    val (a, s2) = t(s)
    f(a)(s2)            // We could also return `f(a)(s)` here.
}
\end{lstlisting}
As before, in order to preserve information, we choose not to discard
the computed value \lstinline!s2!.

The code notation for this \lstinline!flatMap! can be simplified
to
\[
\text{flatMap}\triangleq t^{:S\rightarrow A\times S}\rightarrow f^{:A\rightarrow S\rightarrow B\times S}\rightarrow t\bef\left(a\times s\rightarrow f(a)(s)\right)\quad.
\]


\subsection{Exercises\index{exercises}}

\subsubsection{Exercise \label{subsec:ch-Exercise-0}\ref{subsec:ch-Exercise-0}}

Find the cardinality of the type \lstinline!P = Option[Boolean => Option[Boolean]]!.
Show that \lstinline!P! is equivalent to \lstinline!Option[Boolean] => Boolean!,
and that the equivalence is accidental\index{type equivalence!accidental}
and not \textsf{``}natural\textsf{''}.

\subsubsection{Exercise \label{subsec:ch-Exercise-1-a}\ref{subsec:ch-Exercise-1-a}}

Verify the type equivalences $A+A\cong\bbnum 2\times A$ and $A\times A\cong\bbnum 2\rightarrow A$,
where $\bbnum 2$ denotes the \lstinline!Boolean! type.

\subsubsection{Exercise \label{subsec:ch-Exercise-1}\ref{subsec:ch-Exercise-1}}

Show that $A\Rightarrow(B\vee C)\neq(A\Rightarrow B)\wedge(A\Rightarrow C)$
in constructive and Boolean logic.

\subsubsection{Exercise \label{subsec:ch-Exercise-type-identity-4}\ref{subsec:ch-Exercise-type-identity-4}}

Use known rules to verify the type equivalences without need for proofs:

\textbf{(a)} $\left(A+B\right)\times\left(A\rightarrow B\right)\cong A\times\left(A\rightarrow B\right)+\left(\bbnum 1+A\rightarrow B\right)\quad.$

\textbf{(b)} $\left(A\times(\bbnum 1+A)\rightarrow B\right)\cong\left(A\rightarrow B\right)\times\left(A\rightarrow A\rightarrow B\right)\quad.$

\textbf{(c)} $A\rightarrow\left(\bbnum 1+B\right)\rightarrow C\times D\cong\left(A\rightarrow C\right)\times\left(A\rightarrow D\right)\times\left(A\times B\rightarrow C\right)\times\left(A\times B\rightarrow D\right)\quad.$

\subsubsection{Exercise \label{subsec:ch-Exercise-2}\ref{subsec:ch-Exercise-2}}

Write the type notation for \lstinline!Either[(A, Int), Either[(A, Char), (A, Float)]]!.
Transform this type into an equivalent type of the form $A\times(...)$.

\subsubsection{Exercise \label{subsec:ch-Exercise-3}\ref{subsec:ch-Exercise-3}}

Define a type $\text{OptE}^{T,A}\triangleq\bbnum 1+T+A$ and implement
information-preserving \lstinline!map! and \lstinline!flatMap! for
it, applied to the type parameter $A$. Get the same result using
the equivalent type $(\bbnum 1+A)+T$, i.e., \lstinline!Either[Option[A], T]!.
The required type signatures are
\begin{align*}
\text{map}^{A,B,T} & :\text{OptE}^{T,A}\rightarrow\left(A\rightarrow B\right)\rightarrow\text{OptE}^{T,B}\quad,\\
\text{flatMap}^{A,B,T} & :\text{OptE}^{T,A}\rightarrow(A\rightarrow\text{OptE}^{T,B})\rightarrow\text{OptE}^{T,B}\quad.
\end{align*}


\subsubsection{Exercise \label{subsec:ch-Exercise-4}\ref{subsec:ch-Exercise-4}}

Implement the \lstinline!map! function for the type constructor \lstinline!P[A]!
from Example~\ref{subsec:ch-solvedExample-2}. The required type
signature is $P^{A}\rightarrow\left(A\rightarrow B\right)\rightarrow P^{B}$.
Preserve information as much as possible.

\subsubsection{Exercise \label{subsec:ch-Exercise-4-1}\ref{subsec:ch-Exercise-4-1}}

For the type constructor $Q^{T,A}$ defined in Exercise~\ref{subsec:Exercise-type-notation-1},
define the \lstinline!map! function, preserving information as much
as possible:
\[
\text{map}^{T,A,B}:Q^{T,A}\rightarrow\left(A\rightarrow B\right)\rightarrow Q^{T,B}\quad.
\]


\subsubsection{Exercise \label{subsec:Exercise-disjunctive-6}\ref{subsec:Exercise-disjunctive-6}}

Define a recursive type constructor $\text{Tr}_{3}$ as $\text{Tr}_{3}{}^{A}\triangleq\bbnum 1+A\times A\times A\times\text{Tr}_{3}{}^{A}$
and implement the \lstinline!map! function for it, with the standard
type signature: $\text{map}^{A,B}:\text{Tr}_{3}{}^{A}\rightarrow\left(A\rightarrow B\right)\rightarrow\text{Tr}_{3}{}^{B}\quad.$

\subsubsection{Exercise \label{subsec:ch-Exercise-5}\ref{subsec:ch-Exercise-5}}

Implement fully parametric, information-preserving functions with
the types:

\textbf{(a)} $Z+A\times A\rightarrow(A\rightarrow B)\rightarrow Z+B\times B\quad.$

\textbf{(b)} $A+Z\rightarrow B+Z\rightarrow(A\rightarrow B\rightarrow C)\rightarrow C+Z\quad.$

\textbf{(c)} $P+A\times A\rightarrow(A\rightarrow B)\rightarrow(P\rightarrow A+Q)\rightarrow Q+B\times B\quad.$

\textbf{(d)} $\text{flatMap}^{E,A,B}:\text{Read}^{E,A}\rightarrow(A\rightarrow\text{Read}^{E,B})\rightarrow\text{Read}^{E,B}\quad.$

\textbf{(e)} $\text{State}^{S,A}\rightarrow\left(S\times A\rightarrow B\right)\rightarrow\text{State}^{S,B}\quad.$

\subsubsection{Exercise \label{subsec:ch-Exercise-7}\ref{subsec:ch-Exercise-7}{*}}

Denote $\text{Cont}^{R,T}\triangleq\left(T\rightarrow R\right)\rightarrow R$
and implement the functions:

\textbf{(a)} $\text{map}^{R,T,U}:\text{Cont}^{R,T}\rightarrow(T\rightarrow U)\rightarrow\text{Cont}^{R,U}\quad.$

\textbf{(b)} $\text{flatMap}^{R,T,U}:\text{Cont}^{R,T}\rightarrow(T\rightarrow\text{Cont}^{R,U})\rightarrow\text{Cont}^{R,U}\quad.$

\subsubsection{Exercise \label{subsec:ch-Exercise-8}\ref{subsec:ch-Exercise-8}{*}}

Denote $\text{Sel}^{Z,T}\triangleq\left(T\rightarrow Z\right)\rightarrow T$
and implement the functions:

\textbf{(a)} $\text{map}^{Z,A,B}:\text{Sel}^{Z,A}\rightarrow\left(A\rightarrow B\right)\rightarrow\text{Sel}^{Z,B}\quad.$

\textbf{(b)} $\text{flatMap}^{Z,A,B}:\text{Sel}^{Z,A}\rightarrow(A\rightarrow\text{Sel}^{Z,B})\rightarrow\text{Sel}^{Z,B}\quad.$

\section{Discussion and further developments}

\subsection{Using the Curry-Howard correspondence for writing code}

This chapter shows how the CH correspondence performs two practically
important reasoning tasks: checking whether a type signature can be
implemented as a fully parametric function, and determining whether
two types are equivalent. The first task is accomplished by mapping
type expressions into formulas in the constructive logic and by applying
the proof rules of that logic. The second task is accomplished by
mapping type expressions into \emph{arithmetic} formulas and applying
the ordinary rules of arithmetic.

Fully parametric functions can be often derived from their type signatures
alone. It is useful for a programmer to know that certain type signatures,
such as
\begin{lstlisting}
def f[A, B]: A => (A => B) => B
\end{lstlisting}
have only one possible implementation, while other type signatures,
such as
\begin{lstlisting}
def g[A, B]: A => (B => A) => B
def h[A, B]: ((A => B) => A) => A
\end{lstlisting}
cannot be implemented as fully parametric functions.

Although tools such as the \texttt{curryhoward} library can sometimes
derive code from types, it is more beneficial if a programmer is able
to derive an implementation by hand, or to recognize quickly that
an implementation is impossible. Exercises in this chapter help to
build up the required technique and intuition. For instance, we have
seen heuristics such as \textsf{``}values of parametric types cannot be constructed
from scratch\textsf{''} and \textsf{``}one must hard-code the decision to return a
chosen part of a disjunctive type\textsf{''}. These heuristics can be justified
by the rigorous rules of proof (Section~\ref{subsec:The-rules-of-proof}). 

Throughout this chapter, we required all functions to be fully parametric.
The reason is that the CH correspondence becomes informative only
with parameterized types and with fully parametric functions. For
concrete types, e.g., \lstinline!Int!, one can always produce \emph{some}
value even with no previous data, so the proposition $\mathcal{CH}(\text{Int})$
is always true within any code.

Consider the function \lstinline!(x:Int) => x + 1!. Its type signature,
\lstinline!Int => Int!, is insufficient to specify the code of the
function, because there are many different functions with the same
type signature, such as \lstinline!x => x - 1!, \lstinline!x => x * 2!,
etc. So, deriving code from the type signature \lstinline!Int => Int!
is not a meaningful task. Only a fully parametric type signature,
such as $A\rightarrow\left(A\rightarrow B\right)\rightarrow B$, gives
enough information for possibly deriving the function\textsf{'}s code. If we
permit functions that are not fully parametric, we will not be able
to reason about implementability of type signatures or about code
derivation.

Information about the implementability of type signatures is given
by logical formulas involving ${\cal CH}$-propositions. Validity
of a ${\cal CH}$-proposition ${\cal CH}(T)$ means that we can compute
\emph{some} value of the given type $T$ but does not give any information
about the properties of that value, such as whether it satisfies any
additional laws. This is why type equivalence (which requires the
laws of isomorphism) is not determined by an equivalence of logical
formulas.

It is useful for programmers to be able to reason about types and
transform type expressions to equivalent simpler types before starting
to write code. The type notation introduced in this book is designed
to help programmers to recognize patterns in type expressions and
to reason about them more easily. We have shown that a type equivalence
corresponds to \emph{each} standard arithmetic identity such as $\left(a+b\right)+c=a+\left(b+c\right)$,
$\left(a\times b\right)\times c=a\times(b\times c)$, $1\times a=a$,
$\left(a+b\right)\times c=a\times c+b\times c$, etc. So, we are allowed
to transform and simplify types as if they were arithmetic expressions,
e.g., to rewrite
\[
\bbnum 1\times\left(A+B\right)\times C+D\cong D+A\times C+B\times C\quad.
\]
The type notation makes this reasoning more intuitive (for people
familiar with arithmetic). 

These results apply to all type expressions built up using product
types, disjunctive types (also called \textsf{``}sum\textsf{''} types because they
correspond to arithmetic sums), and function types (also called \textsf{``}exponential\textsf{''}
types because they correspond to arithmetic exponentials). Type expressions
that contain only products and sum types may be called \textbf{polynomial}\index{polynomial type}\index{types!polynomial types}.
Type expressions that also contain function types may be called \textbf{exponential-polynomial}\index{exponential-polynomial types}\index{types!exponential-polynomial}.\footnote{Polynomial types are often called \textsf{``}algebraic data types\index{algebraic data type}\textsf{''}.}
This book focuses on exponential-polynomial types because they are
sufficient for almost all design patterns used in functional programming.

There are no type constructions corresponding to subtraction or division,
so equations such as 
\begin{align*}
\left(1-t\right)\times\left(1+t\right) & =1-t\times t\quad\text{or }\quad\frac{t+t\times t}{t}=1+t
\end{align*}
do not directly yield any type equivalences. However, consider this
well-known formula,
\[
\frac{1}{1-t}=1+t+t^{2}+t^{3}+...+t^{n}+...\quad.
\]
At first sight, this formula appears to involve subtraction, division,
and an infinite series, and thus cannot be directly translated into
a type equivalence. However, the formula can be rewritten as
\begin{equation}
\frac{1}{1-t}\triangleq L(t)=1+t+t^{2}+t^{3}+...+t^{n}\times L(t)\quad,\label{eq:ch-example-type-formula-list}
\end{equation}
which is finite and only contains additions and multiplications. So,
Eq.~(\ref{eq:ch-example-type-formula-list}) can be translated into
a type equivalence:
\begin{equation}
L^{A}\cong1+A+A\times A+A\times A\times A+...+\underbrace{A\times...\times A}_{n\text{ times}}\times\,L^{A}\quad.\label{eq:ch-example-type-expansion-list}
\end{equation}
This type formula (with $n=1$) is equivalent to a recursive definition
of the type constructor \lstinline!List!,
\[
\text{List}^{A}\triangleq1+A\times\text{List}^{A}\quad.
\]
The type equivalence~(\ref{eq:ch-example-type-expansion-list}) suggests
that we may view the recursive type \lstinline!List! as an \textsf{``}infinite
disjunction\textsf{''} describing lists of zero, one, etc., elements.

\subsection{Implications for designing new programming languages}

The functional programming paradigm assumes that programmers will
use the six standard type constructions (Section~\ref{subsec:Type-notation-and-standard-type-constructions})
and the eight standard code constructions (Section~\ref{subsec:The-rules-of-proof}).
These constructions are foundational in the sense that they are used
to express all design patterns of functional programming. A language
that does not directly support some of these constructions cannot
be considered a functional programming language.

A remarkable consequence of the CH correspondence is that the type
system of any programming language (functional or not) is mapped into
a \emph{certain} \emph{logic}, i.e., a system of logical operations
and proof rules. A logical operation will correspond to each of the
type constructions available in the programming language; a proof
rule will correspond to each of the available code constructions.
Functional programming languages that support all the standard type
and code constructions \textemdash{} for instance, OCaml, Haskell,
F\#, Scala, Swift, Rust, \textemdash{} will be mapped into the constructive
logic with all standard logical operations available ($True$, $False$,
disjunction, conjunction, and implication). 

Languages such as C, C++, Java, C\# are mapped into logics that do
not have the disjunction operation or the constants $True$ and $False$.
In other words, these languages are mapped into \emph{incomplete}
logics where some theorems will not be provable. (If ${\cal CH}(A)$
is true but not provable, a value of type $A$ is not directly computable
by programs, although it could have been.) Incompleteness of the logic
of types will make a programming language unable to express certain
computations, e.g., directly handle data that belongs to a disjoint
domain. 

Languages such as Python, JavaScript, Ruby, Clojure do not enforce
type checking and so are mapped to \emph{inconsistent} logics where
any proposition can be derived \textemdash{} even propositions normally
considered $False$ may be derived from $True$. The CH correspondence
will map such derivations to code that appears to compute a certain
value (since the $\mathcal{CH}$-proposition appears to be $True$)
although that value is not actually available. In practice, such code
will \emph{crash} because the computed value has a wrong type, is
\textsf{``}null\textsf{''}, or is a pointer to an invalid memory location.

None of these errors will happen in a programming language whose logic
of types is complete and consistent, provided that types are checked
at compile time. 

So, the CH correspondence gives a mathematically justified procedure
for designing new programming languages. The procedure has the following
steps:
\begin{itemize}
\item Choose a formal logic that is complete and free of inconsistencies.
\item For each logical operation, provide a type construction in the language.
\item For each proof rule or axiom of the logic, provide a code construction
in the language.
\end{itemize}
Mathematicians have studied different logics: e.g., modal logic, temporal
logic, or linear logic. Compared with the constructive logic, these
other logics have some additional operations. (For instance, modal
logic adds the operations \textsf{``}necessarily\textsf{''} and \textsf{``}possibly\textsf{''}, and
temporal logic adds the operation \textsf{``}until\textsf{''}.) For each logic, mathematicians
have determined the minimal complete sets of operations, axioms, and
proof rules that do not lead to inconsistency. Programming language
designers can choose a logic and translate it into a minimal programming
language where the code is guaranteed \emph{not to crash} as long
as types match. This mathematical guarantee (known as \index{type safety}\textbf{type
safety}) is a powerful help for programmers since it automatically
prevents a large set of programming errors. So, programmers will benefit
if their programming language is designed using the CH correspondence.

Practically useful programming languages will, of course, introduce
many more features than the minimal, mathematically necessary constructions
derived from the chosen logic. Programmers will still benefit from
type safety as long as their programs stay within the mathematically
consistent subset of the language. For Scala, a \textsf{``}safe\textsf{''} subset
is identified by the \texttt{scalazzi} project.\footnote{\texttt{\href{https://github.com/scalaz/scalazzi}{https://github.com/scalaz/scalazzi}}}

At present, it is not fully understood whether a practical programming
language can use, say, modal or linear logic as its logic of types.
Experience suggests that, at least, the operations of the plain constructive
logic should be available. So, it appears that the six type constructions
and the eight code constructions will remain available in all future
languages of functional programming. 

\subsection{Uses of the void type (\texttt{Nothing})}

The \index{void type}void type (Scala\textsf{'}s \lstinline!Nothing!) corresponds
to the logical constant $False$. There are few practical uses of
the void type. One use case is for a branch of a \lstinline!match!/\lstinline!case!
expression that does not return a value because it throws an \index{exception}exception.
A \lstinline!throw! expression is defined as if it returns a value
of type \lstinline!Nothing!. We can then pretend to convert that
\textsf{``}value\textsf{''} (which will never be actually computed) into a value of
any other type. (See Example~\ref{subsec:ch-Example-type-identity-0-to-A}
that implements a function \lstinline!absurd[A]: Nothing => A!.) 

To see how this trick is used, consider this code defining a value
\lstinline!x!,
\begin{lstlisting}
val x: Double = if (t >= 0.0) math.sqrt(t) else { throw new Exception("error") }
\end{lstlisting}
The \lstinline!else! branch does not return a value, but \lstinline!x!
is declared to be of type \lstinline!Double!. For this code to type-check,
both branches must return values of the same type. So, the compiler
needs to pretend that the \lstinline!else! branch also returns a
value of type \lstinline!Double!. The compiler first assigns the
type \lstinline!Nothing! to the expression \lstinline!throw ...!
and then automatically uses the conversion \lstinline!Nothing => Double!
to convert that type to \lstinline!Double!. In this way, types will
match in the definition of the value \lstinline!x!. 

We will not use exceptions in this book. The functional programming
paradigm does not use exceptions because their presence significantly
complicates reasoning about code.

As another example of using the void type, suppose an external library
implements a function
\begin{lstlisting}
def parallel_run[E, A, B](f: A => Either[E, B]) = ???
\end{lstlisting}
that performs some parallel computations using a given function $f$.
In general, the library supports functions $f^{:A\rightarrow E+B}$
that may return an error of type $E$ or a result of type $B$. Suppose
we know that a particular function $f$ never fails to compute its
result. To express that knowledge in code, we may explicitly set the
type parameter $E$ to the void type \lstinline!Nothing! when applying
\lstinline!parallel_run!:
\begin{lstlisting}
parallel_run[Nothing, A, B](f)  // Types match only when values f(a) always are of the form Right(b). 
\end{lstlisting}
Returning an error is now impossible (the type \lstinline!Nothing!
has no values). If the function \lstinline!parallel_run! is fully
parametric, it will work in the same way with all types $E$, including
$E=\bbnum 0$. The code implements our intention via type parameters,
giving a compile-time guarantee of correct results.

So far, none of our examples involved the logical \textbf{negation}\index{negation (in logic)}
operation. It is defined as 
\[
\neg\alpha\triangleq\alpha\Rightarrow False\quad,
\]
and its practical use is as limited as that of $False$ and the void
type. However, logical negation plays an important role in Boolean
logic, which we will discuss next.

\subsection{Relationship between Boolean logic and constructive logic\label{subsec:Relationship-between-Boolean} }

We have seen that some true theorems of Boolean logic are not true
in constructive logic. For example, the Boolean identities $\neg\left(\neg\alpha\right)=\alpha$
and $\left(\alpha\Rightarrow\beta\right)=(\neg\alpha\vee\beta)$ do
not hold in the constructive logic. However, any theorem of constructive
logic is also a theorem of Boolean logic. The reason is that all eight
rules of constructive logic (Section~\ref{subsec:The-rules-of-proof})
are also true in Boolean logic.

To verify that a formula is true in Boolean logic, we only need to
check that the value of the formula is $True$ for all possible truth
values ($True$ or $False$) of its variables. A sequent such as $\alpha,\beta\vdash\gamma$
is true in Boolean logic if and only if $\gamma=True$ under the assumption
that $\alpha=\beta=True$. So, the sequent $\alpha,\beta\vdash\gamma$
is translated into the Boolean formula 
\[
\alpha,\beta\vdash\gamma=\left(\left(\alpha\wedge\beta\right)\Rightarrow\gamma\right)=\left(\neg\alpha\vee\neg\beta\vee\gamma\right)\quad.
\]
Table~\ref{tab:Proof-rules-of-constructive-and-boolean} translates
all proof rules of Section~\ref{subsec:The-rules-of-proof} into
Boolean formulas. The first two lines are axioms, while the subsequent
lines are Boolean theorems that can be verified by calculation.

\begin{table}
\begin{centering}
\begin{tabular}{|c|c|}
\hline 
\textbf{\small{}Constructive logic} & \textbf{\small{}Boolean logic}\tabularnewline
\hline 
\hline 
{\small{}$\frac{}{\Gamma\vdash{\cal CH}(\bbnum 1)}\quad(\text{create unit})$} & {\small{}$\neg\Gamma\vee True=True$}\tabularnewline
\hline 
{\small{}$\frac{~}{\Gamma,\alpha\vdash\alpha}\quad(\text{use arg})$} & {\small{}$\neg\Gamma\vee\neg\alpha\vee\alpha=True$}\tabularnewline
\hline 
{\small{}$\frac{\Gamma,\alpha\vdash\beta}{\Gamma\vdash\alpha\Rightarrow\beta}\quad(\text{create function})$} & {\small{}$\left(\neg\Gamma\vee\neg\alpha\vee\beta\right)=\left(\neg\Gamma\vee\left(\alpha\Rightarrow\beta\right)\right)$}\tabularnewline
\hline 
{\small{}$\frac{\Gamma\vdash\alpha\quad\quad\Gamma\vdash\alpha\Rightarrow\beta}{\Gamma\vdash\beta}\quad(\text{use function})$} & {\small{}$\left(\left(\neg\Gamma\vee\alpha\right)\wedge\left(\neg\Gamma\vee\left(\alpha\Rightarrow\beta\right)\right)\right)\Rightarrow\left(\neg\Gamma\vee\beta\right)$}\tabularnewline
\hline 
{\small{}$\frac{\Gamma\vdash\alpha\quad\quad\Gamma\vdash\beta}{\Gamma\vdash\alpha\wedge\beta}\quad(\text{create tuple})$} & {\small{}$\left(\neg\Gamma\vee\alpha\right)\wedge\left(\neg\Gamma\vee\beta\right)=\left(\neg\Gamma\vee\left(\alpha\wedge\beta\right)\right)$}\tabularnewline
\hline 
{\small{}$\frac{\Gamma\vdash\alpha\wedge\beta}{\Gamma\vdash\alpha}\quad(\text{use tuple-}1)$} & {\small{}$\left(\neg\Gamma\vee\left(\alpha\wedge\beta\right)\right)\Rightarrow\left(\neg\Gamma\vee\alpha\right)$}\tabularnewline
\hline 
{\small{}$\frac{\Gamma\vdash\alpha}{\Gamma\vdash\alpha\vee\beta}\quad(\text{create Left})$} & {\small{}$\left(\neg\Gamma\vee\alpha\right)\Rightarrow\left(\neg\Gamma\vee\left(\alpha\vee\beta\right)\right)$}\tabularnewline
\hline 
{\small{}$\frac{\Gamma\vdash\alpha\vee\beta\quad\quad\Gamma,\alpha\vdash\gamma\quad\quad\Gamma,\beta\vdash\gamma}{\Gamma\vdash\gamma}\quad(\text{use Either})$} & {\small{}$\left(\left(\neg\Gamma\vee\alpha\vee\beta\right)\wedge\left(\neg\Gamma\vee\neg\alpha\vee\gamma\right)\wedge\left(\neg\Gamma\vee\neg\beta\vee\gamma\right)\right)\Rightarrow\left(\neg\Gamma\vee\gamma\right)$}\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{Proof rules of constructive logic are true also in the Boolean logic.\label{tab:Proof-rules-of-constructive-and-boolean}}
\end{table}

To simplify the calculations, note that all terms in the formulas
contain the operation $\left(\neg\Gamma\vee...\right)$ corresponding
to the context $\Gamma$. Now, if $\Gamma$ is $False$, the entire
formula becomes automatically $True$, and there is nothing else to
check. So, it remains to verify the formula in case $\Gamma=True$,
and then we can simply omit all instances of $\neg\Gamma$ in the
formulas. Let us show the Boolean derivations for the rules \textsf{``}$\text{use function}$\textsf{''}
and \textsf{``}$\text{use Either}$\textsf{''}; other formulas are checked in a similar
way. 
\begin{align*}
{\color{greenunder}\text{formula \textsf{``}use function\textsf{''}}:}\quad & \left(\alpha\wedge\left(\alpha\Rightarrow\beta\right)\right)\Rightarrow\beta\\
{\color{greenunder}\text{use Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & =\gunderline{\neg}(\alpha\,\gunderline{\wedge}\,(\neg\alpha\,\gunderline{\vee}\,\beta))\vee\beta\\
{\color{greenunder}\text{de Morgan\textsf{'}s laws}:}\quad & =\gunderline{\neg\alpha\vee(\alpha\wedge\neg\beta)}\vee\beta\\
{\color{greenunder}\text{identity }p\vee(\neg p\wedge q)=p\vee q\text{ with }p=\neg\alpha\text{ and }q=\beta:}\quad & =\neg\alpha\vee\gunderline{\neg\beta\vee\beta}\\
{\color{greenunder}\text{axiom \textsf{``}use arg\textsf{''}}:}\quad & =True\quad.
\end{align*}
\begin{align*}
{\color{greenunder}\text{formula \textsf{``}use Either\textsf{''}}:}\quad & \left(\left(\alpha\vee\beta\right)\wedge\left(\alpha\Rightarrow\gamma\right)\wedge\left(\beta\Rightarrow\gamma\right)\right)\Rightarrow\gamma\\
{\color{greenunder}\text{use Eq.~(\ref{eq:ch-definition-of-implication-in-Boolean-logic})}:}\quad & =\neg\left(\left(\alpha\vee\beta\right)\wedge\left(\neg\alpha\vee\gamma\right)\wedge\left(\neg\beta\vee\gamma\right)\right)\vee\gamma\\
{\color{greenunder}\text{de Morgan\textsf{'}s laws}:}\quad & =\left(\neg\alpha\wedge\neg\beta\right)\vee\gunderline{\left(\alpha\wedge\neg\gamma\right)}\vee\gunderline{\left(\beta\wedge\neg\gamma\right)}\vee\gamma\\
{\color{greenunder}\text{identity }p\vee(\neg p\wedge q)=p\vee q:}\quad & =\gunderline{\left(\neg\alpha\wedge\neg\beta\right)\vee\alpha}\vee\beta\vee\gamma\\
{\color{greenunder}\text{identity }p\vee(\neg p\wedge q)=p\vee q:}\quad & =\gunderline{\neg\alpha\vee\alpha}\vee\beta\vee\gamma\\
{\color{greenunder}\text{axiom \textsf{``}use arg\textsf{''}}:}\quad & =True\quad.
\end{align*}
Since each proof rule of the constructive logic is translated into
a true formula in Boolean logic, it follows that a proof tree in the
constructive logic will be translated into a tree of Boolean formulas
that have value $True$ for each axiom or proof rule. The result is
that any constructive proof for a sequent such as $\emptyset\vdash f(\alpha,\beta,\gamma)$
is translated into a chain of Boolean implications that look like
this,
\[
True=(...)\Rightarrow(...)\Rightarrow...\Rightarrow f(\alpha,\beta,\gamma)\quad.
\]
Since $\left(True\Rightarrow\alpha\right)=\alpha$, this chain proves
the Boolean formula $f(\alpha,\beta,\gamma)$.

For example, the proof tree shown in Figure~\ref{fig:Proof-of-the-sequent-example-2}
is translated into
\begin{align*}
{\color{greenunder}\text{axiom \textsf{``}use arg\textsf{''}}:}\quad & True=\left(\neg\left(\left(\alpha\Rightarrow\alpha\right)\Rightarrow\beta\right)\vee\neg\alpha\vee\alpha\right)\\
{\color{greenunder}\text{rule \textsf{``}create function\textsf{''}}:}\quad & \quad\Rightarrow\neg\left(\left(\alpha\Rightarrow\alpha\right)\Rightarrow\beta\right)\vee\left(\alpha\Rightarrow\alpha\right)\quad.\\
{\color{greenunder}\text{axiom \textsf{``}use arg\textsf{''}}:}\quad & True=\neg\left(\left(\alpha\Rightarrow\alpha\right)\Rightarrow\beta\right)\vee\left(\left(\alpha\Rightarrow\alpha\right)\Rightarrow\beta\right)\quad.\\
{\color{greenunder}\text{rule \textsf{``}use function\textsf{''}}:}\quad & True\Rightarrow\left(\neg\left(\left(\alpha\Rightarrow\alpha\right)\Rightarrow\beta\right)\vee\beta\right)\\
{\color{greenunder}\text{rule \textsf{``}create function\textsf{''}}:}\quad & \quad\Rightarrow\left(\left(\left(\alpha\Rightarrow\alpha\right)\Rightarrow\beta\right)\Rightarrow\beta\right)\quad.
\end{align*}

It is easier to check Boolean truth than to find a proof tree in constructive
logic (or to establish that no proof tree exists). So, if we find
that a formula is not true in Boolean logic, we know it is also not
true in constructive logic. This gives us a quick way of proving that
some type signatures are not implementable as fully parametric functions.
In addition to formulas shown in Table~\ref{tab:Logical-formulas-not-Boolean-theorems}
(Section~\ref{subsec:ch-Motivation-and-first-examples}), further
examples of formulas that are not true in Boolean logic are
\begin{align*}
 & \forall\alpha.\,\alpha\quad,\\
 & \forall(\alpha,\beta).\,\alpha\Rightarrow\beta\quad,\\
 & \forall(\alpha,\beta).\,(\alpha\Rightarrow\beta)\Rightarrow\beta\quad.
\end{align*}

Table~\ref{tab:Proof-rules-of-constructive-and-boolean} uses the
Boolean identity $\left(\alpha\Rightarrow\beta\right)=(\neg\alpha\vee\beta)$,
which does not hold in the constructive logic, to translate the constructive
axiom \textsf{``}$\text{use arg}$\textsf{''} into the Boolean axiom $\neg\alpha\vee\alpha=True$.
The formula $\neg\alpha\vee\alpha=True$ is known as the \textbf{law
of excluded middle}\footnote{\texttt{\href{https://en.wikipedia.org/wiki/Law_of_excluded_middle}{https://en.wikipedia.org/wiki/Law\_of\_excluded\_middle}}}\index{law of excluded middle}
and is equivalent to saying that any proposition $\alpha$ is either
true or false. It is remarkable that the constructive logic \emph{does
not have} the law of excluded middle; it is neither an axiom nor a
derived theorem of constructive logic. 

To see why, consider what it would mean for $\neg\alpha\vee\alpha=True$
to hold in the constructive logic. The negation operation, $\neg\alpha$,
is defined as the implication $\alpha\Rightarrow False$. So, the
logical formula $\forall\alpha.\,\neg\alpha\vee\alpha$ corresponds
to the type $\forall A.\,\left(A\rightarrow\bbnum 0\right)+A$. Can
we compute a value of this type in a fully parametric function? We
need to compute either a value of type $A\rightarrow\bbnum 0$ or
a value of type $A$; this decision needs to be made in advance independently
of $A$, because the code of a fully parametric function must operate
in the same way for all types. Should we return $A$ or $A\rightarrow\bbnum 0$?
We certainly cannot compute a value of type $A$ from scratch, since
$A$ is an arbitrary type. As we have seen in Example~\ref{subsec:ch-Example-type-identity-A-0},
a value of type $A\rightarrow\bbnum 0$ exists if the type $A$ is
itself $\bbnum 0$; but we do not know whether $A=\bbnum 0$. In any
case, a fully parametric function needs to have the same code for
all types $A$. Since there are no values of type $\bbnum 0$, and
the type parameter $A$ could be, say, \lstinline!Int!, we cannot
compute a value of type $A\rightarrow\bbnum 0$.

Example~\ref{subsec:ch-Example-type-identity-A-0} showed that the
type $A\rightarrow\bbnum 0$ is equivalent to $\bbnum 0$ if $A$
is not itself void ($A\not\cong\bbnum 0$), and to $\bbnum 1$ otherwise.
Surely, any type $A$ is either void or not void. So, why exactly
is it impossible to implement a value of the type $\left(A\rightarrow\bbnum 0\right)+A$?
We could say that if $A$ is void then $\left(A\rightarrow\bbnum 0\right)\cong\bbnum 1$
is not void, and so one of the types in the disjunction $\left(A\rightarrow\bbnum 0\right)+A$
should be non-void (i.e., have values).

However, this reasoning is incorrect. It is insufficient to show that
a value \textsf{``}should exist\textsf{''}; the real requirement is to \emph{compute}
a value of type $\left(A\rightarrow\bbnum 0\right)+A$ via a fully
parametric function. That function\textsf{'}s code may not decide what to do
depending on whether $A$ is void \textemdash{} the code is required
to be the same for all types $A$ (void or not). As we have seen,
that code is impossible to write.

In Boolean logic, it is sufficient to prove that a value \textsf{``}should
exist\textsf{''} (or that the non-existence of a value is contradictory in
some way). However, any practically useful program needs to \textsf{``}construct\textsf{''},
i.e., compute, actual values and return them. The \textsf{``}constructive\index{constructive logic}\textsf{''}
logic got its name from this requirement. So, it is the constructive
logic (not the Boolean logic) that provides correct reasoning about
the types of values computable by fully parametric functional programs.

Without the requirement of full parametricity, we \emph{could} implement
the law of excluded middle\index{law of excluded middle}. Special
features of Scala (\textsf{``}reflection\textsf{''}, \textsf{``}type tags\textsf{''}, and \textsf{``}type
casts\textsf{''}) allow us to compare types as values and to determine what
type was given to a type parameter when a function is applied:
\begin{lstlisting}[mathescape=true]
import scala.reflect.runtime.universe._
def getType[T: TypeTag]: Type = weakTypeOf[T]   // Convert the type parameter T into a special value.
def equalTypes[A: TypeTag, B: TypeTag]: Boolean = getType[A] =:= getType[B] // Compare types A and B.

def excludedMiddle[A: TypeTag]: Either[A, A => Nothing] =  // excludedMiddle has type ${\color{dkgreen}\forall A.\,\left(A\rightarrow\bbnum 0\right)+A}$.
   if (equalTypes[A, Nothing]) Right((identity _).asInstanceOf[A => Nothing])    // Return ${\color{dkgreen}\text{id}:\bbnum 0\rightarrow\bbnum 0}$.
   else if (equalTypes[A, Int]) Left(123.asInstanceOf[A])          // Produce some value of type Int.
   else if (equalTypes[A, Boolean]) Left(true.asInstanceOf[A]) // Produce some value of type Boolean.
   else ???                  // Need to write many more definitions to support all other Scala types.

scala> excludedMiddle[Int]
res0: Either[Int,Int => Nothing] = Left(123)

scala> excludedMiddle[Nothing]
res1: Either[Nothing,Nothing => Nothing] = Right(<function1>) 
\end{lstlisting}
In this code, we check whether $A=\bbnum 0$; if so, we can implement
$A\rightarrow\bbnum 0$ as an identity function of type $\bbnum 0\rightarrow\bbnum 0$.
Otherwise, we know that $A$ is one of the existing Scala types (\lstinline!Int!,
\lstinline!Boolean!, etc.), which are not void and have values that
we can simply write down one by one in the subsequent code. 

Explicit\index{type casts} \textbf{type casts}, such as \lstinline!123.asInstanceOf[A]!,
are needed because the Scala compiler cannot know that \lstinline!A!
is \lstinline!Int! in the scope where we return \lstinline!Left(123)!.
Without a type cast, the compiler will not accept \lstinline!123!
as a value of type \lstinline!A! in that scope.

The method \lstinline!asInstanceOf! is dangerous: the code \lstinline!x.asInstanceOf[T]!
disables all type checking for the given value \lstinline!x!, telling
the Scala compiler to believe that \lstinline!x! has type \lstinline!T!
even when the type \lstinline!T! is inconsistent with the actually
given code of \lstinline!x!. Programs written in this way will compile
but may give unexpected results or crash because of errors that would
have been prevented by type checking. It is rare that a Scala program
truly requires type casts or explicit comparisons of type parameters.
In this book, we will avoid writing such code.
